natDegree_cyclotomic — Mathlib

English

For any natural n and nontrivial ring R, the natural degree of Φ_n over R equals φ(n).

Русский

Для любого n и ненулевого кольца R естественная степень Φ_n над R равна φ(n).

LaTeX

$$$$\operatorname{natDegree}(\mathrm{cyclotomic} \ n \ R) = \varphi(n).$$$$

Lean4

/-- The natural degree of `cyclotomic n` is `totient n`. -/
theorem natDegree_cyclotomic (n : ℕ) (R : Type*) [Ring R] [Nontrivial R] : (cyclotomic n R).natDegree = Nat.totient n :=
  by rw [natDegree, degree_cyclotomic]; norm_cast

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