rightHomologyMap_smul — Mathlib

English

The right homology map respects scalar multiplication: rightHomologyMap (a • φ) = a • rightHomologyMap φ.

Русский

Правая карта гомологии сохраняет умножение на скаляр: rightHomologyMap (a • φ) = a • rightHomologyMap φ.

LaTeX

$$$\mathrm{rightHomologyMap}(a\cdot φ) = a\cdot \mathrm{rightHomologyMap}(φ)$$$

Lean4

@[simp]
theorem rightHomologyMap_smul : rightHomologyMap (a • φ) = a • rightHomologyMap φ :=
  rightHomologyMap'_smul _ _ _ _

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