Diff — Pythagorean triple

Revision #2635 → #3197 · back to history

addedGaussian integersa4216beb4191

addedUnique factorization of Gaussian integers85d15a8a67c3

addedArithmetic progressions of three squares ↔ Pythagorean triplesa0811375b1c9

addedConsecutive-squares difference divisible by 24cb7dfbfdca13

modifiedNo isosceles Pythagorean triplesa2458e354c22

Field	From #2635	To #3197
note	Not formalized.	Follows from irrationality of √2; not stated as a Pythagorean-triple lemma in Mathlib.