id — Mathlib · SciLib

English

For the identity automorphism of L, the cyclotomic character χ₀(n, id) equals 1 in (Z/nZ)ˣ.

Русский

Для тождественного автоморфизма χ₀(n, id) = 1 в (Z/nZ)ˣ.

LaTeX

$$$\\chi_{0}(n, \\mathrm{id}) = 1$$$

Lean4

theorem id : χ₀ n (RingEquiv.refl L) = 1 :=
  by
  refine (toFun_unique n (RingEquiv.refl L) 1 <| fun t ↦ ?_).symm
  have : 1 ≤ Fintype.card { x // x ∈ rootsOfUnity n L } := Fin.size_positive'
  obtain (h | h) := this.lt_or_eq
  · have := Fact.mk h
    simp [ZMod.val_one]
  · have := Fintype.card_le_one_iff_subsingleton.mp h.ge
    obtain rfl : t = 1 := Subsingleton.elim t 1
    simp

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