smul — Mathlib

English

The left homology functor is linear over R: it is a linear functor.

Русский

Левый гомологический функтор линейный по отношению к R: это линейный функтор.

LaTeX

$$$\text{Functor.Linear}_R(\text{leftHomologyFunctor}(C))$$$

Lean4

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

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