ρ_self_inv_apply

Mathlib.CategoryTheory.Action.Concrete

URI: https://scilib.ai/kg/mathlib#Action.ρ_self_inv_apply

English

For any g in G and x in A.V, A.ρ g (A.ρ g⁻¹ x) = x.

Русский

Для любого g∈G и x∈A.V выполняется A.ρ g (A.ρ g⁻¹ x) = x.

LaTeX

$$$\forall g\in G,\forall x\in A.V\; A.\rho(g)(A.\rho(g^{-1})(x)) = x.$$$

Lean4

@[simp]
theorem ρ_self_inv_apply (g : G) (x : A.V) : A.ρ g (A.ρ g⁻¹ x) = x :=
  show (A.ρ g * A.ρ g⁻¹) x = x by simp [← map_mul]

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru