leftHomologyMap_smul — Mathlib

English

More generally, leftHomologyMap respects scalar multiplication for all data, i.e., leftHomologyMap (a • φ) = a • leftHomologyMap φ.

Русский

Более общо: карта левой гомологии сохраняет умножение на скаляр: leftHomologyMap (a • φ) = a • leftHomologyMap φ.

LaTeX

$$$\mathrm{leftHomologyMap}(a\cdot \varphi) = a\cdot \mathrm{leftHomologyMap}(\varphi)$$$

Lean4

@[simp]
theorem leftHomologyMap_smul : leftHomologyMap (a • φ) = a • leftHomologyMap φ :=
  leftHomologyMap'_smul _ _ _ _

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