smul_zero — Mathlib

English

A generic auxiliary smul on the free additive monoid level corresponds to the TMUL construction after the quotient.

Русский

Обобщённое вспомогательное умножение на уровне свободного аддитивного моноида соответствует конструированию TMUL после факторизации.

LaTeX

$$$ \\mathrm{SMul}.\\mathrm{aux} \\; r \\; (\\mathrm{of}(m,n)) = (r \\cdot m) \\otimes n. $$$

Lean4

protected theorem smul_zero (r : R') : r • (0 : M ⊗[R] N) = 0 :=
  AddMonoidHom.map_zero _

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