card_nthRoots_one — Mathlib

English

For any automorphism f, μ raised to the image of f in ZMod n equals f(μ).

Русский

Для любого автоморфизма f выполняется: μ возведено в степень, соответствующую образу f в Z/nZ, равно f(μ).

LaTeX

$$$\mu^{(h\mu.autToPow R f : \mathbb{Z}/n\mathbb{Z})}.val = f(\mu)$$$

Lean4

/-- The cardinality of the multiset `nthRoots ↑n (1 : R)` is `n`
if there is a primitive root of unity in `R`. -/
theorem card_nthRoots_one {ζ : R} {n : ℕ} (h : IsPrimitiveRoot ζ n) : Multiset.card (nthRoots n (1 : R)) = n := by
  rw [card_nthRoots h, if_pos ⟨ζ, h.pow_eq_one⟩]

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