English
Let K be a field with a primitive cube root of unity η and η^2 + η + 1 = 0. For any S' in the three-gen Fermat system, the sum of cubes S'.a^3 + S'.b^3 factors as (S'.a + S'.b)(S'.a + η S'.b)(S'.a + η^2 S'.b).
Русский
Пусть K — поле, содержащее примитивное корень тождества η третьей степени, и η^2 + η + 1 = 0. Для любого S' из системы трёх ген Fermat'а сумма кубов S'.a^3 + S'.b^3 раскладывается как (S'.a + S'.b)(S'.a + η S'.b)(S'.a + η^2 S'.b).
LaTeX
$$$S'.a^3 + S'.b^3 = (S'.a + S'.b)(S'.a + \eta S'.b)(S'.a + \eta^2 S'.b)$$$
Lean4
/-- Given `S' : Solution'`, the key factorization of `S'.a ^ 3 + S'.b ^ 3`. -/
theorem a_cube_add_b_cube_eq_mul : S'.a ^ 3 + S'.b ^ 3 = (S'.a + S'.b) * (S'.a + η * S'.b) * (S'.a + η ^ 2 * S'.b) :=
by
symm
calc
_ = S'.a ^ 3 + S'.a ^ 2 * S'.b * (η ^ 2 + η + 1) + S'.a * S'.b ^ 2 * (η ^ 2 + η + η ^ 3) + η ^ 3 * S'.b ^ 3 := by
ring
_ = S'.a ^ 3 + S'.a ^ 2 * S'.b * (η ^ 2 + η + 1) + S'.a * S'.b ^ 2 * (η ^ 2 + η + 1) + S'.b ^ 3 := by
simp [hζ.toInteger_cube_eq_one]
_ = S'.a ^ 3 + S'.b ^ 3 := by rw [eta_sq]; ring
