int_cyclotomic_rw — Mathlib

English

For n ≠ 0, cyclotomic n ℤ equals the chosen int_coeff_of_cyclotomic' evaluated at n.

Русский

Если n ≠ 0, то cyclotomic n ℤ равен выбираемому целочисленному коэффициентному полиному int_coeff_of_cyclotomic' (Complex.isPrimitiveRoot_exp n h).choose.

LaTeX

$$$\operatorname{cyclotomic}(n,\mathbb{Z}) = (\operatorname{int\_coeff\_of\_cyclotomic'}(\operatorname{Complex.isPrimitiveRoot\_exp} n h)).\choose$ (при $n \neq 0$)$$

Lean4

theorem int_cyclotomic_rw {n : ℕ} (h : n ≠ 0) :
    cyclotomic n ℤ = (int_coeff_of_cyclotomic' (Complex.isPrimitiveRoot_exp n h)).choose :=
  by
  simp only [cyclotomic, h, dif_neg, not_false_iff]
  ext i
  simp only [coeff_map, Int.cast_id, eq_intCast]

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