cyclotomic_six — Mathlib

English

Over any ring R, cyclotomic 6 R equals X^2 − X + 1.

Русский

Над любым кольцом R циклотомический 6 равен X^2 − X + 1.

LaTeX

$$cyclotomic(6, R) = X^2 - X + 1$$

Lean4

@[simp]
theorem cyclotomic_six (R : Type*) [Ring R] : cyclotomic 6 R = X ^ 2 - X + 1 :=
  by
  suffices cyclotomic 6 ℤ = X ^ 2 - X + 1 by
    rw [← map_cyclotomic_int, this]
    simp
  apply mul_right_cancel₀ (cyclotomic_ne_zero 2 ℤ)
  rw [show 6 = 2 * 3 by rfl, ← cyclotomic_expand_eq_cyclotomic_mul Nat.prime_three (by norm_num1)]
  simp; ring

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