smul — Mathlib

English

There is a scalar action of $R$ on HomologyMapData: given a homology map data for φ, one obtains the corresponding data for $a·φ$ by scaling both sides by $a$.

Русский

Существует действие скаляра над $R$ на данные гомологического отображения: для данного данных гомологии на φ получают соответствующие данные для $a·φ$ путём масштабирования обеих частей на $a$.

LaTeX

$$$\\text{smul}: \\mathrm{HomologyMapData}(\\varphi,h_1,h_2) \\times R \\to \\mathrm{HomologyMapData}(a\\cdot \\varphi,h_1,h_2)$ with left/right components scaled by $a$$$

Lean4

/-- Given a homology map data for a morphism `φ`, this is the induced homology
map data for `a • φ`. -/
@[simps]
def smul (a : R) : HomologyMapData (a • φ) h₁ h₂
    where
  left := γ.left.smul a
  right := γ.right.smul a

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