ρ_inv_self_apply

Mathlib.CategoryTheory.Action.Concrete

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

English

For any g in G and x in A.V, A.ρ g⁻¹ (A.ρ g x) = x; i.e., the action is by a group.

Русский

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

LaTeX

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

Lean4

@[simp]
theorem ρ_inv_self_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