self_inv_apply

Mathlib.RepresentationTheory.Basic

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

English

Equivalently, ρ(g^{-1})(ρ(g)(x)) = x for all g ∈ G, x ∈ V.

Русский

Эквивалентно: для всех g ∈ G и x ∈ V выполняется ρ(g^{-1})(ρ(g)(x)) = x.

LaTeX

$$ρ(g^{-1}) ∘ ρ(g) = id_V$$

Lean4

@[simp]
theorem self_inv_apply (g : G) (x : V) : ρ g (ρ g⁻¹ x) = x := by simp [← Module.End.mul_apply, ← map_mul]

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

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

Разделы

Аффилиация

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