cyclesMap'_smul — Mathlib

English

The induced left homology map respects scalar multiplication: leftHomologyMap (a • φ) = a • leftHomologyMap φ.

Русский

Индуцированная карта левой гомологии сохраняет скаляры: leftHomologyMap (a • φ) = a • leftHomologyMap φ.

LaTeX

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

Lean4

@[simp]
theorem cyclesMap'_smul : cyclesMap' (a • φ) h₁ h₂ = a • cyclesMap' φ h₁ h₂ :=
  by
  have γ : LeftHomologyMapData φ h₁ h₂ := default
  simp only [(γ.smul a).cyclesMap'_eq, LeftHomologyMapData.smul_φK, γ.cyclesMap'_eq]

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