H1AddEquivOfIsTrivial_symm_tmul — Mathlib

English

The inverse of H1AddEquivOfIsTrivial evaluated at a simple tensor is the corresponding H1π image of a single group element.

Русский

Обратное к H1AddEquivOfIsTrivial, применённое к тензору-части, равняется H1π изображения элемента группы.

LaTeX

$$theorem H1AddEquivOfIsTrivial_symm_tmul (g : G) (a : A) :\n (H1AddEquivOfIsTrivial A).symm (Additive.ofMul (Abelianization.of g) ⊗ₜ[ℤ] a) =\n H1π A ((cycles₁IsoOfIsTrivial A).inv <| single g a) :=\n by rfl$$

Lean4

@[simp]
theorem H1AddEquivOfIsTrivial_symm_tmul (g : G) (a : A) :
    (H1AddEquivOfIsTrivial A).symm (Additive.ofMul (Abelianization.of g) ⊗ₜ[ℤ] a) =
      H1π A ((cycles₁IsoOfIsTrivial A).inv <| single g a) :=
  by rfl

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