indToCoindAux_snd_mul_inv — Mathlib

English

For all g in G and x in A, the composition ρ(g^{-1}) after ρ(g) fixes x, i.e., ρ(g^{-1})(ρ(g)(x)) = x.

Русский

Для любого g ∈ G и x ∈ A верно ρ(g^{-1})(ρ(g)(x)) = x.

LaTeX

$$$A.ρ(g^{-1}) (A.ρ(g) x) = x$$$

Lean4

@[simp]
theorem indToCoindAux_snd_mul_inv (g₁ g₂ g₃ : G) (a : A) :
    indToCoindAux A g₁ a (g₂ * g₃⁻¹) = indToCoindAux A (g₁ * g₃) a g₂ :=
  by
  rcases em ((QuotientGroup.rightRel S).r (g₂ * g₃⁻¹) g₁) with ⟨s, hs⟩ | h
  · simp [S.1.smul_def, mul_assoc, ← eq_mul_inv_iff_mul_eq.1 hs]
  · rw [indToCoindAux_of_not_rel (h := h), indToCoindAux_of_not_rel]
    exact mt (fun ⟨s, hs⟩ => ⟨s, by simpa [S.1.smul_def, eq_mul_inv_iff_mul_eq, mul_assoc]⟩) h

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