norm_comp_self — Mathlib

English

For all g ∈ G, the averaging operator commutes with ρ(g): norm ρ ∘ ρ g = norm ρ.

Русский

Для каждого элемента gG усредняющий оператор коммутирует с действием ρ(g): norm ρ ∘ ρ(g) = norm ρ.

LaTeX

$$$\\forall g \\in G:\\; ρ(g) \\circ \\operatorname{norm} \\rho = \\operatorname{norm} \\rho$$$

Lean4

@[simp]
theorem norm_comp_self (g : G) : norm ρ ∘ₗ ρ g = norm ρ :=
  by
  ext
  simpa [norm] using Fintype.sum_bijective (· * g) (Group.mulRight_bijective g) _ _ <| by simp

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