PythagoreanTriple.eq
theorem
∀ {x y z : ℤ}, PythagoreanTriple x y z → x * x + y * y = z * zPythagorean Triple Identity: x2 + y2 = z2
...
LeanSearch needs your feedback
To continually improve the search quality, LeanSearch needs your feedback on the results.
Take the search term pythagorean theorem as an example. Right now, the results include theorems concerning pythagorean triples, sin2 x + cos2 x = 1, and different versions of Pythagorean theorem. However, the user most likely wants to find either WithLp.prod_norm_sq_eq_of_L2, or the elegantly and epically named EuclideanGeometry.dist_sq_eq_dist_sq_add_dist_sq_iff_angle_eq_pi_div_two.
This certainly showed some space for improvement. In order to improve the relevance and ranking of results, we need to collect your feedback.
There are three kinds of feedbacks you can provide:
- Whenever you spot an item that is right on the spot but is ranked too low, you can click the upvote button to suggest LeanSearch to move it up.
- On the other hand, if an item is relevant but probably shouldn't be among the top results, click downvote.
- For some items that are completely irrelevant, be sure to click the irrelevant button.
In this example, PythagoreanTriple.eq should receive a downvote, both WithLp.prod_norm_sq_eq_of_L2 and EuclideanGeometry.dist_sq_eq_dist_sq_add_dist_sq_iff_angle_eq_pi_div_two should be upvoted, and the rest should probably be left as-is.
Real.Angle.cos_sq_add_sin_sq
theorem
∀ (θ : Real.Angle), θ.cos ^ 2 + θ.sin ^ 2 = 1
Pythagorean Identity for Angles Modulo 2π
...
Real.cos_sq_add_sin_sq
theorem
∀ (x : ℝ), Real.cos x ^ 2 + Real.sin x ^ 2 = 1
Pythagorean Identity for Real Numbers
...
Real.sin_sq_add_cos_sq
theorem
∀ (x : ℝ), Real.sin x ^ 2 + Real.cos x ^ 2 = 1
Pythagorean Identity for Real Numbers
...
WithLp.prod_norm_sq_eq_of_L2
theorem
∀ {α : Type u_2} {β : Type u_3} [inst : SeminormedAddCommGroup α] [inst_1 : SeminormedAddCommGroup β]
(x : WithLp 2 (α × β)), ‖x‖ ^ 2 = ‖x.1‖ ^ 2 + ‖x.2‖ ^ 2Pythagorean Theorem for L2 Norm on Product Spaces
...
Complex.cos_sq_add_sin_sq
theorem
∀ (x : ℂ), Complex.cos x ^ 2 + Complex.sin x ^ 2 = 1
Pythagorean Identity for Complex Numbers
...
PythagoreanTriple
definition
ℤ → ℤ → ℤ → Prop
Pythagorean triple
...
EuclideanGeometry.dist_sq_eq_dist_sq_add_dist_sq_iff_angle_eq_pi_div_two
theorem
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
[inst_3 : NormedAddTorsor V P] (p1 p2 p3 : P),
dist p1 p3 * dist p1 p3 = dist p1 p2 * dist p1 p2 + dist p3 p2 * dist p3 p2 ↔
EuclideanGeometry.angle p1 p2 p3 = Real.pi / 2Pythagorean theorem (distance and angle form)
...
What data are collected?
The search term you enter is always collected.
Your feedback on items and the associated search term is collected.
NO personal data of any kind (IP address, geolocation, browser, OS) will be collected. We use cookies only to record the association between feedbacks and search terms.
How will the data be used?
The data will only be used for academic purposes. We will use the data to improve the search quality of LeanSearch and construct better benchmarks.