instIsMulTorsionFreeMultiplicativeOfIsAddTorsionFree

English

If α is an AddMonoid and IsAddTorsionFree α, then Multiplicative α is IsMulTorsionFree.

Русский

Если α — аддитивный моноид и IsAddTorsionFree α, то Multiplicative α безторсионна.

LaTeX

$$$[\text{AddMonoid α}]\ [\mathrm{IsAddTorsionFree}\ α] : \mathrm{IsMulTorsionFree}(\mathrm{Multiplicative}\ α)$$$

Lean4

instance [AddMonoid α] [IsAddTorsionFree α] : IsMulTorsionFree (Multiplicative α) where
  pow_left_injective _ := nsmul_right_injective (M := α)

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