comp — Mathlib

English

The cyclotomic character χ₀ is multiplicative: χ₀(n, g ∘ h) = χ₀(n,g) χ₀(n,h) for automorphisms g,h.

Русский

Характер циклотомический χ₀ по умножению: χ₀(n,g∘h) = χ₀(n,g) χ₀(n,h).

LaTeX

$$$\\chi_{0}(n, g\\circ h) = \\chi_{0}(n,g) \\cdot \\chi_{0}(n,h)$$$

Lean4

theorem comp (g h : L ≃+* L) : χ₀ n (g * h) = χ₀ n g * χ₀ n h :=
  by
  refine (toFun_unique n (g * h) _ <| fun ζ ↦ ?_).symm
  change g (h (ζ : Lˣ)) = _
  rw [toFun_spec, ← Subgroup.coe_pow, toFun_spec, mul_comm, Subgroup.coe_pow, ← pow_mul, ← Subgroup.coe_pow]
  congr 2
  norm_cast
  simp only [pow_eq_pow_iff_modEq, ← ZMod.natCast_eq_natCast_iff, ZMod.natCast_val, Nat.cast_mul,
    ZMod.cast_mul (m := orderOf ζ) orderOf_dvd_card]

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