norm_apply — Mathlib

English

For a finite group G and an AddChar ψ: G → α into a normed ring with nonnegative norm, the norm of ψ at any argument is 1.

Русский

Для конечной группы G и символьного характеристического отображения ψ: G → α нормa ψ(x) равна 1 для любого x.

LaTeX

$$$\\|\\psi(x)\\| = 1$ for all $x \\in G$.$$

Lean4

@[simp]
theorem norm_apply {G : Type*} [AddLeftCancelMonoid G] [Finite G] (ψ : AddChar G α) (x : G) : ‖ψ x‖ = 1 :=
  (ψ.toMonoidHom.isOfFinOrder <| isOfFinOrder_of_finite _).norm_eq_one

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