starComp_eq_inv — Mathlib

English

Post-composing an additive character with complex conjugation yields the inverse character: starComp φ = φ^{-1}.

Русский

После композиции аддитивной характеристики со взятием комплексного сопряжения получается обратная характеристика: starComp φ = φ^{-1}.

LaTeX

$$starComp(φ) = φ^{-1}$$

Lean4

/-- Post-composing an additive character to `ℂ` with complex conjugation gives the inverse
character. -/
theorem starComp_eq_inv (hR : 0 < ringChar R) {φ : AddChar R ℂ} : (starRingEnd ℂ).compAddChar φ = φ⁻¹ :=
  by
  ext1 a
  simp only [RingHom.toMonoidHom_eq_coe, MonoidHom.coe_compAddChar, MonoidHom.coe_coe, Function.comp_apply, inv_apply']
  have H := Complex.norm_eq_one_of_mem_rootsOfUnity <| φ.val_mem_rootsOfUnity a hR
  exact (Complex.inv_eq_conj H).symm

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