ρ_self_inv_apply — Mathlib

English

For any g in G, the endomorphism ρ(g) has inverse ρ(g^{-1}) and their composition is the identity.

Русский

Для любого g ∈ G отображение ρ(g) на A имеет обратное ρ(g^{-1}); их композиция равна тождественному отображению.

LaTeX

$$$A.\rho g \circ A.\rho g^{-1} = \mathrm{id}$, for all $g \in G$$$

Lean4

@[deprecated Representation.self_inv_apply (since := "2025-05-09")]
theorem ρ_self_inv_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, mul_inv_cancel, map_one, Module.End.one_apply]

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