Vector spaces are torsion-free #
In this file, we show that any module over a division semiring is torsion-free.
Note that more generally any reflexive module is torsion-free.
@[instance 100]
instance
DivisionSemiring.to_moduleIsTorsionFree
{𝕜 : Type u_1}
{M : Type u_2}
[DivisionSemiring 𝕜]
[AddCommMonoid M]
[Module 𝕜 M]
:
Any (semi)vector space is torsion-free.