card_rootsOfUnity' — Mathlib

English

If there exists a primitive root of order n in R, then the number of n-th roots of unity in R is exactly n.

Русский

Если в кольце R существует примитивный корень порядка n, то число n-ых корней единицы в R ровно равно n.

LaTeX

$$$\\#\\{\\text{rootsOfUnity}(n,R)\\} = n$$$

Lean4

/-- A variant of `IsPrimitiveRoot.card_rootsOfUnity` for `ζ : Rˣ`. -/
theorem card_rootsOfUnity' {n : ℕ} [NeZero n] (h : IsPrimitiveRoot ζ n) : Fintype.card (rootsOfUnity n R) = n :=
  by
  let e := h.zmodEquivZPowers
  have : Fintype (Subgroup.zpowers ζ) := Fintype.ofEquiv _ e.toEquiv
  calc
    Fintype.card (rootsOfUnity n R) = Fintype.card (Subgroup.zpowers ζ) := Fintype.card_congr <| by rw [h.zpowers_eq]
    _ = Fintype.card (ZMod n) := (Fintype.card_congr e.toEquiv.symm)
    _ = n := ZMod.card n

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