colimitHasSMul — Mathlib

English

The zero element in the colimit is represented by the zero in each component.

Русский

Нуль в пределе задаётся нулём в каждом компоненте.

LaTeX

$$$$ 0 = M.{\\text{mk}} F \\langle j, 0\\rangle $$$$

Lean4

/-- Scalar multiplication in the colimit. See also `colimitSMulAux`. -/
instance colimitHasSMul : SMul R (M F) where
  smul r
    x := by
    refine Quot.lift (colimitSMulAux F r) ?_ x
    intro x y h
    apply colimitSMulAux_eq_of_rel
    apply Types.FilteredColimit.rel_of_colimitTypeRel
    exact h

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