Revision #3197 → #3710 · back to history
modified(3, 4, 5) is a Pythagorean triplef48b4d435e58
| Field | From #3197 | To #3710 |
|---|
| note | No standalone lemma instantiating `PythagoreanTriple 3 4 5` was found. | No standalone lemma instantiating `PythagoreanTriple 3 4 5` was found in `Mathlib/NumberTheory/PythagoreanTriples.lean`. |
modifiedScaling a Pythagorean triple2f98112bb10a
| Field | From #3197 | To #3710 |
|---|
| note | `PythagoreanTriple.mul` shows scaling by `k` preserves the triple; `mul_iff` gives the iff form. | `PythagoreanTriple.mul` shows scaling by `k` preserves the triple; `mul_iff` gives the iff form for nonzero `k`. |
addedParity in primitive triple (odd square ≡ 1 mod 4)91f1a1b8475c
modifiedHypotenuse form 4n+1fd10a1207685
| Field | From #3197 | To #3710 |
|---|
| note | Sum-of-two-squares facts (`Nat.Prime.sq_add_sq`, `Nat.eq_sq_add_sq_iff`) give the general result; not specialized to hypotenuses. | Sum-of-two-squares facts (`Nat.Prime.sq_add_sq`, `Nat.eq_sq_add_sq_iff`) give the general result; not specialized to Pythagorean hypotenuses. |
modifiedAcute angles not rational degreesc7d1d1109639
| Field | From #3197 | To #3710 |
|---|
| note | Niven-type irrationality of Pythagorean angles is not formalized. | Niven's theorem on rational values of trig functions is not currently formalized as a Mathlib lemma applicable to Pythagorean angles. |
addedPick's theorem (used for lattice triangle area)5e413e261b83
modifiedNo isosceles Pythagorean triplesa2458e354c22
| Field | From #3197 | To #3710 |
|---|
| mathlib.decl | — | irrational_sqrt_two |
| mathlib.module | — | Mathlib.NumberTheory.Real.Irrational |
| note | Follows from irrationality of √2; not stated as a Pythagorean-triple lemma in Mathlib. | Follows from irrationality of `√2` (`irrational_sqrt_two`); not stated as a Pythagorean-triple lemma in Mathlib. |
| status | not_formalized | partial |