Theorems · Inductive type · commutative algebra

Module.IsTorsionFree

(R : Type u_1) → (M : Type u_3) → [inst : Semiring R] → [inst_1 : AddCommMonoid M] → [Module R M] → Prop

An R-module M is torsion-free if scalar multiplication by an element r : R is injective if multiplication (on R) by r is. For domains, this is equivalent to the usual condition of r • m = 0 → r = 0 ∨ m = 0. See smul_eq_zero.

Defined in

Mathlib.Algebra.Module.Torsion.Free

Cited by

600 results in Mathlib

Foundations

Depth 2 from the axioms, rests on 4 definitions · uses no axioms

Assumes

SemiringAddCommMonoidModule