Right triangles with whole-number sides

A Pythagorean triple: three whole numbers where x² + y² = z² — the 3-4-5 family.

Start with a concrete example

A right triangle can have whole-number sides 3,4,5 because 3²+4²=5². The equation records the right angle; not every three whole numbers make such a triangle.

A small check: try the idea

Think with the concrete example above. You can try again.

Do 3,4,5 satisfy the right-triangle equation?

Read the answer and reasoning

Yes; 9+16=25. The rule adds squares, not the side lengths directly: 3²+4²=5².

Build the idea in three steps

A Pythagorean triple is three whole numbers sitting on a right triangle, and the definition spends exactly one line on it: PythagoreanTriple x y z just means x * x + y * y = z * z.
Check the family: 3 ^ 2 + 4 ^ 2 = 9 + 16 = 25 = 5 ^ 2, so (3, 4, 5) is a triple — and multiplying every side by 2 gives another: (6, 8, 10).
The legs are interchangeable: pythagoreanTriple_comm swaps x and y, because x * x + y * y = y * y + x * x. The proof is delta to unfold the one-line definition, then rw [add_comm].

A small example

(5, 12, 13) joins the family: 25 + 144 = 169. Here the word "diagram" and the word "equation" are the same thing — that is the quiet power of a one-line definition.

Lean definition · original excerpt

Mathlib · db584cd · PythagoreanTriples.lean

42/-- Three integers `x`, `y`, and `z` form a Pythagorean triple if `x * x + y * y = z * z`. -/43def PythagoreanTriple (x y z : ℤ) : Prop :=44  x * x + y * y = z * z45 46/-- Pythagorean triples are interchangeable, i.e `x * x + y * y = y * y + x * x = z * z`.47This comes from additive commutativity. -/48theorem pythagoreanTriple_comm {x y z : ℤ} : PythagoreanTriple x y z ↔ PythagoreanTriple y x z := by49  delta PythagoreanTriple50  rw [add_comm]

How to read this Lean

There is no hidden machinery: the predicate is one equation about integers, and eq, symm and mul are built directly on it in the lines below. The older pages folded fourth powers into squares so that a⁴ + b⁴ = c² would land in exactly this shape — PythagoreanTriple (a ^ 2) (b ^ 2) c, right-triangle legs that are themselves squares. Descending to the school diagram of the 3-4-5 triangle is precisely how the exponent-four case will start manufacturing its smaller suspects.

Original source ↗ · L42–50 Open the complete saved source

Where this idea is used

7. The veterans’ cabinet

Right triangles with whole-number sides

Start with a concrete example

A small check: try the idea

Build the idea in three steps

A small example

Lean definition · original excerpt

How to read this Lean

Where this idea is used

Mika’s help desk

One thing at a time

In simpler words

A small clue