smul_map_inv_div_map_inv_of_isMulCocycle₂

English

For f: G × G → M with IsMulCocycle₂ f, we have g • f(g^{-1}, g) / f(g, g^{-1}) = f(1,1) / f(g,1) for all g.

Русский

Для f: G × G → M с IsMulCocycle₂: g • f(g^{-1}, g) / f(g, g^{-1}) = f(1,1) / f(g,1).

LaTeX

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

Lean4

theorem smul_map_inv_div_map_inv_of_isMulCocycle₂ {f : G × G → M} (hf : IsMulCocycle₂ f) (g : G) :
    g • f (g⁻¹, g) / f (g, g⁻¹) = f (1, 1) / f (g, 1) :=
  by
  have := hf g g⁻¹ g
  simp only [mul_inv_cancel, inv_mul_cancel, map_one_fst_of_isMulCocycle₂ hf g] at this
  exact div_eq_div_iff_mul_eq_mul.2 this.symm

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