instIsCancelAdd — Mathlib

English

If R is an additive cancelative ring, then the MonoidAlgebra R[M] is also additive cancelative.

Русский

Если R обладает свойством отменности по сложению, то MonoidAlgebra R[M] также обладает этим свойством.

LaTeX

$$$\text{IsCancelAdd}(\mathrm{MonoidAlgebra}\;R\;M)$$$

Lean4

@[to_additive]
instance instIsCancelAdd [IsCancelAdd R] : IsCancelAdd (MonoidAlgebra R M) :=
  inferInstanceAs <| IsCancelAdd <| M →₀ R

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