cube_sub_one_eq_mul — Mathlib

English

For any x in NumberField.RingOfIntegers K, x^3 − 1 factors as (x − 1)(x − η)(x − η^2).

Русский

Для любого x из NumberField.RingOfIntegers K выражение x^3 − 1 разлагается как (x − 1)(x − η)(x − η^2).

LaTeX

$$$x^{3} - 1 = (x - 1)(x - \eta)(x - \eta^{2})$$$

Lean4

/-- We have that `x ^ 3 - 1 = (x - 1) * (x - η) * (x - η ^ 2)`. -/
theorem cube_sub_one_eq_mul : x ^ 3 - 1 = (x - 1) * (x - η) * (x - η ^ 2) :=
  by
  symm
  calc
    _ = x ^ 3 - x ^ 2 * (η ^ 2 + η + 1) + x * (η ^ 2 + η + η ^ 3) - η ^ 3 := by ring
    _ = x ^ 3 - x ^ 2 * (η ^ 2 + η + 1) + x * (η ^ 2 + η + 1) - 1 := by simp [hζ.toInteger_cube_eq_one]
    _ = x ^ 3 - 1 := by rw [eta_sq_add_eta_add_one hζ]; ring

Похожие утверждения