norm_self_apply

Mathlib.RepresentationTheory.Basic

URI: https://scilib.ai/kg/mathlib#Representation.norm_self_apply

English

For each g ∈ G and x ∈ V, applying ρ(g) to norm ρ x leaves norm ρ x unchanged: ρ(g)(norm ρ x) = norm ρ x.

Русский

Для каждого g ∈ G и x ∈ V выполняется ρ(g)(norm ρ x) = norm ρ x.

LaTeX

$$$\\rho(g) (\\operatorname{norm}_{\\rho} x) = \\operatorname{norm}_{\\rho} x$$$

Lean4

@[simp]
theorem norm_self_apply (g : G) (x : V) : norm ρ (ρ g x) = norm ρ x :=
  LinearMap.ext_iff.1 (norm_comp_self _ _) x

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru