inv_apply_eq_conj — Mathlib

English

For every finite group G and additive character ψ: G → K, the value ψ(x) lies on the unit circle, hence ψ(x)^{-1} = conj(ψ(x)) for all x ∈ G.

Русский

Для каждого конечного множества G и аддитивного символа ψ: G → K, значения ψ(x) лежат на окружности единичной длины, следовательно ψ(x)^{-1} = conj(ψ(x)) для всех x ∈ G.

LaTeX

$$$ (\\psi(x))^{-1} = \\overline{\\psi(x)} $$$

Lean4

theorem inv_apply_eq_conj [AddLeftCancelMonoid G] (ψ : AddChar G K) (x : G) : (ψ x)⁻¹ = conj (ψ x) :=
  RCLike.inv_eq_conj <| norm_apply _ _

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