natSMulWithZero — Mathlib

English

For any AddMonoid A, the natural-number scalars act on A in a way that respects zero: nsmul_zero and zero_nsmul.

Русский

Для любого AddMonoid A естественные числа действуют на A так, чтобы выполнялись nsmul_zero и zero_nsmul.

LaTeX

$$$\\text{AddMonoid}(A)\\quad\\Rightarrow\\quad \\text{SMulWithZero } \\mathbb{N} A\\;\\text{with }\\text{smul\_zero} = \\_root_.nsmul\_zero,\\; \\text{zero\_smul} = zero\_nsmul$$$

Lean4

instance natSMulWithZero [AddMonoid A] : SMulWithZero ℕ A
    where
  smul_zero := _root_.nsmul_zero
  zero_smul := zero_nsmul

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