inv_self_apply — Mathlib

English

For a representation ρ of a group G on V, ρ(g) and ρ(g^{-1}) are inverse linear maps: ρ(g) ∘ ρ(g^{-1}) = id_V.

Русский

Для отображения ρ группы G на V линейные отображения ρ(g) и ρ(g^{-1}) являются обратными: ρ(g) ∘ ρ(g^{-1}) = id_V.

LaTeX

$$ρ(g) ∘ ρ(g^{-1}) = LinearMap.id$$

Lean4

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

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