instIsAddTorsionFreeAdditiveOfIsMulTorsionFree

English

If α is a monoid and IsMulTorsionFree α, then Additive α is IsAddTorsionFree.

Русский

Пусть α — моноид и выполнение IsMulTorsionFree α. Тогда Additive α безторсионна по отношению к сложению.

LaTeX

$$$[\text{Monoid }\alpha]\ [\mathrm{IsMulTorsionFree}\ \alpha] \Rightarrow \mathrm{IsAddTorsionFree}(\mathrm{Additive}\ \alpha)$$$

Lean4

instance [Monoid α] [IsMulTorsionFree α] : IsAddTorsionFree (Additive α) where
  nsmul_right_injective _ := pow_left_injective (M := α)

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