ρ_self_inv_apply — Mathlib

English

For g ∈ G, the composition A.ρ g with A.ρ g⁻¹ yields the identity; equivalently, ρ g followed by its inverse is the identity on A.

Русский

Для любого g ∈ G композиция A.ρ g с A.ρ g⁻¹ даёт тождество на A.

LaTeX

$$$A.\rho g \circ A.\rho g^{-1} = \mathrm{id}$$$

Lean4

@[deprecated Representation.self_inv_apply (since := "2025-05-09")]
theorem ρ_self_inv_apply {G : Type u} [Group G] {A : Rep k 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]

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