A wider net with a unit

To descend, first prove more: a³ + b³ = u·c³ with an arbitrary unit u.

Start with a concrete example

Changing x³+y³ to x³−y³ introduces a minus sign. A generalized statement can track such allowed factors explicitly instead of pretending the formula stayed unchanged.

A small check: try the idea

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

If a sign changes from x³+y³ to x³−y³, may the proof silently ignore it?

Read the answer and reasoning

No; allowed coefficient changes must be tracked. For x=y=1, the first expression is 2 and the second is 0. A generalized claim must state exactly which factors it allows.

Build the idea in three steps

The descent proves a generalized claim with explicit conditions: in 𝓞 K, a ^ 3 + b ^ 3 = u * c ^ 3 is impossible for any unit u when c ≠ 0, λ divides c but neither a nor b, and a and b are coprime. These conditions matter: the unrestricted equation does have solutions.
The extra freedom u is the very room a descent needs: its decisive step multiplies by units, so the net must catch solutions even when the factor wobbles.
The lemma FermatLastTheoremForThree_of_FermatLastTheoremThreeGen then walks this wider claim back down to FermatLastTheoremFor 3, the exact statement of the case.

A small example

A unit is an element with an inverse: in the ordinary integers only 1 and −1. The wider statement tolerates wobbles by such factors, the way a sound can change its loudness without changing the melody.

Lean definition · original excerpt

Mathlib · db584cd · Three.lean

158/-- `FermatLastTheoremForThreeGen` is the statement that `a ^ 3 + b ^ 3 = u * c ^ 3` has no159nontrivial solutions in `𝓞 K` for all `u : (𝓞 K)ˣ` such that `¬ λ ∣ a`, `¬ λ ∣ b` and `λ ∣ c`.160The reason to consider `FermatLastTheoremForThreeGen` is to make a descent argument working. -/161def FermatLastTheoremForThreeGen : Prop :=162  ∀ a b c : 𝓞 K, ∀ u : (𝓞 K)ˣ, c ≠ 0 → ¬ λ ∣ a → ¬ λ ∣ b → λ ∣ c → IsCoprime a b →163    a ^ 3 + b ^ 3 ≠ u * c ^ 3164 165/-- To prove `FermatLastTheoremFor 3`, it is enough to prove `FermatLastTheoremForThreeGen`. -/166lemma FermatLastTheoremForThree_of_FermatLastTheoremThreeGen167    [NumberField K] [IsCyclotomicExtension {3} ℚ K] :168    FermatLastTheoremForThreeGen hζ → FermatLastTheoremFor 3 := by

How to read this Lean

Read the docstring first: it says plainly why the wider statement exists — to make the descent argument work. The definition lists the conditions: c ≠ 0, λ must not divide a or b, λ must divide c, a and b are coprime. The λ ∣ c hypothesis mirrors the case split of the previous page: the divisibility by three lands on one of the three numbers, and the argument arranges for it to be c.

Original source ↗ · L158–168 Open the complete saved source

Where this idea is used

2. The case of three 7. The veterans’ cabinet

A wider net with a unit

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