instIsAddTorsionFree — Mathlib

English

If M is Add-torsion-free, then the Finsupp type ι →₀ M is also Add-torsion-free.

Русский

Если M — аддитивно тождественно свободная группа, то Finsupp(ι, M) тоже свободна отTORSION.

LaTeX

$$$\text{IsAddTorsionFree}(M) \Rightarrow \text{IsAddTorsionFree}(\,\iota \to_{0} M\,)$$$

Lean4

instance instIsAddTorsionFree [IsAddTorsionFree M] : IsAddTorsionFree (ι →₀ M) :=
  DFunLike.coe_injective.isAddTorsionFree coeFnAddHom

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