degree_cyclotomic' — Mathlib

English

If a primitive n-th root exists in R, then the degree of cyclotomic' n R is φ(n).

Русский

Если существует примитивный корень n-й степени в R, то степень cyclotomic' n R равна φ(n).

LaTeX

$$$\operatorname{degree}(\operatorname{cyclotomic}'(n,R)) = \operatorname{totient}(n)$$$

Lean4

/-- The degree of `cyclotomic' n R` is `totient n` if there is a primitive root of unity in `R`. -/
theorem degree_cyclotomic' {ζ : R} {n : ℕ} (h : IsPrimitiveRoot ζ n) : (cyclotomic' n R).degree = Nat.totient n := by
  simp only [degree_eq_natDegree (cyclotomic'_ne_zero n R), natDegree_cyclotomic' h]

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