homologyMap'_smul — Mathlib

English

The primed homology map is $R$-linear in the morphism, i.e., $homologyMap'(a·φ) = a·homologyMap'(φ)$.

Русский

Прямая гомологическая карта с апострофом является $R$-линейной по морфизму: $homologyMap'(a·φ) = a·homologyMap'(φ)$.

LaTeX

$$$\\mathrm{homologyMap}'(a\\cdot \\varphi,h_1,h_2) = a \\cdot \\mathrm{homologyMap}'(\\varphi,h_1,h_2)$$$

Lean4

@[simp]
theorem homologyMap'_smul : homologyMap' (a • φ) h₁ h₂ = a • homologyMap' φ h₁ h₂ :=
  leftHomologyMap'_smul _ _ _ _

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