map_inv_of_isMulCocycle₁ — Mathlib

English

Let f: G → M satisfy IsMulCocycle₁. Then for every g ∈ G, g • f(g^{-1}) = f(g)^{-1}.

Русский

Пусть f: G → M удовлетворяет IsMulCocycle₁. Тогда для каждого g: g • f(g^{-1}) = f(g)^{-1}.

LaTeX

$$$\\forall g \\in G,\\; g \\cdot f(g^{-1}) = f(g)^{-1}$$$

Lean4

@[scoped simp]
theorem map_inv_of_isMulCocycle₁ {f : G → M} (hf : IsMulCocycle₁ f) (g : G) : g • f g⁻¹ = (f g)⁻¹ := by
  rw [← mul_eq_one_iff_eq_inv, ← map_one_of_isMulCocycle₁ hf, ← mul_inv_cancel g, hf g g⁻¹]

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