star_eq_inv — Mathlib

English

The conjugate of a multiplicative character valued in ℂ is its inverse: star χ = χ^{-1}.

Русский

Сопряжение мультисимвола с комплексными значениями равно его обратному.

LaTeX

$$star χ = χ^{-1}$$

Lean4

/-- The conjugate of a multiplicative character with values in `ℂ` is its inverse. -/
theorem star_eq_inv (χ : MulChar R ℂ) : star χ = χ⁻¹ :=
  by
  cases nonempty_fintype Rˣ
  ext1 a
  simp only [inv_apply_eq_inv']
  exact (inv_eq_conj <| norm_eq_one_of_mem_rootsOfUnity <| χ.apply_mem_rootsOfUnity a).symm

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