natDegree_cyclotomic_le — Mathlib

English

For any ring R and natural n, the natural degree of Φ_n R is at most φ(n); if R is nontrivial, the degree equals φ(n).

Русский

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

LaTeX

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

Lean4

/-- The natural degree of `cyclotomic n` is at most `totient n`.

If the base ring is nontrivial, then the degree is exactly `φ n`,
otherwise it's zero. -/
theorem natDegree_cyclotomic_le {R : Type*} [Ring R] {n : ℕ} : natDegree (cyclotomic n R) ≤ n.totient :=
  by
  nontriviality R
  rw [natDegree_cyclotomic]

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