indToCoindAux_fst_mul_inv — Mathlib

English

For all g ∈ G, the map ρ(g) has inverse ρ(g^{-1}); thus ρ(g) ∘ ρ(g^{-1}) = id and ρ(g^{-1}) ∘ ρ(g) = id.

Русский

Для каждого g ∈ G отображение ρ(g) имеет обратное ρ(g^{-1}); следовательно ρ(g) ∘ ρ(g^{-1}) = id и ρ(g^{-1}) ∘ ρ(g) = id.

LaTeX

$$$A.ρ(g) ∘ A.ρ(g^{-1}) = \mathrm{id}$ and $A.ρ(g^{-1}) ∘ A.ρ(g) = \mathrm{id}$$$

Lean4

@[simp]
theorem indToCoindAux_fst_mul_inv (g₁ g₂ g₃ : G) (a : A) :
    indToCoindAux A (g₁ * g₂⁻¹) a g₃ = indToCoindAux A g₁ a (g₃ * g₂) := by
  simpa using (indToCoindAux_snd_mul_inv g₁ g₃ g₂⁻¹ a).symm

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