ρ_inv_self_apply — Mathlib

English

For any group element g, the operator ρ(g) is invertible and its inverse is ρ(g^{-1}); hence ρ(g^{-1}) ∘ ρ(g) = id and ρ(g) ∘ ρ(g^{-1}) = id.

Русский

Для любого элемента группы g оператор ρ(g) обратим и его обратный равен ρ(g^{-1}); следовательно ρ(g^{-1}) ∘ ρ(g) = id и ρ(g) ∘ ρ(g^{-1}) = id.

LaTeX

$$$A.\rho(g^{-1}) \circ A.\rho(g) = \mathrm{id}$ для всех $g \in G$$$

Lean4

@[deprecated Representation.inv_self_apply (since := "2025-05-09")]
theorem ρ_inv_self_apply {G : Type u} [Group G] {A : FDRep R G} (g : G) (x : A) : A.ρ g⁻¹ (A.ρ g x) = x :=
  show (A.ρ g⁻¹ * A.ρ g) x = x by rw [← map_mul, inv_mul_cancel, map_one, Module.End.one_apply]

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