Documentation

Mathlib.Algebra.Module.Torsion.Field

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]

Any (semi)vector space is torsion-free.