ρ_inv_self_apply — Mathlib

English

For a representation A and g ∈ G, A.ρ g⁻¹ followed by A.ρ g yields the identity on A; i.e., the composite is the identity endomorphism.

Русский

Для любого A и g ∈ G композиция A.ρ g⁻¹ ∘ A.ρ g равна единичному концу на A.

LaTeX

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

Lean4

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

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