ofRootOfUnity_spec — Mathlib

English

The value of the constructed character on the chosen generator equals the specified root of unity ζ.

Русский

Значение сконструированного символа на заданном генераторе g равно ζ.

LaTeX

$$ofRootOfUnity hζ hg g = ζ$$

Lean4

theorem ofRootOfUnity_spec {ζ : Rˣ} (hζ : ζ ∈ rootsOfUnity (Fintype.card Mˣ) R) {g : Mˣ}
    (hg : ∀ x, x ∈ Subgroup.zpowers g) : ofRootOfUnity hζ hg g = ζ := by
  simp only [ofRootOfUnity, ofUnitHom_eq, equivToUnitHom_symm_coe, monoidHomOfForallMemZpowers_apply_gen]

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