intSMulWithZero — Mathlib

English

For any AddGroup A, the integers act on A with zero, i.e., there is SMulWithZero ℤ A given by zsmul_zero and zero_zsmul.

Русский

Для любого AddGroup A существуют действия целых чисел на A с нулем: zsmul_zero и zero_zsmul.

LaTeX

$$$\\text{AddGroup } A \\Rightarrow \\text{SMulWithZero } \\mathbb{Z} A\\;\\text{with }\\text{smul\_zero} = zsmul\_zero,\\; \\text{zero\_smul} = zero\_zsmul$$$

Lean4

instance intSMulWithZero [AddGroup A] : SMulWithZero ℤ A
    where
  smul_zero := zsmul_zero
  zero_smul := zero_zsmul

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