addAction — Mathlib

English

If α is a Monoid and β carries a MulAction by α, there is a canonical AddAction of Additive α on β, defined by zero_vadd = one_smul and add_vadd = mul_smul.

Русский

Если α — моноид, и β имеет MulAction α, то существует каноническое AddAction Additive α на β, задаваемое zero_vadd = one_smul и add_vadd = mul_smul.

LaTeX

$$$\\text{zero\\_vadd} = \\text{one\\_smul}, \\quad \\text{add\\_vadd} = \\text{mul\\_smul}$$$

Lean4

instance addAction [Monoid α] [MulAction α β] : AddAction (Additive α) β
    where
  zero_vadd := MulAction.one_smul
  add_vadd := MulAction.mul_smul (α := α)

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