Theorems · Theorem · commutative algebra

smul_left_injective

∀ (R : Type u_1) {M : Type u_3} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {m : M}
  [IsCancelMulZero R] [Module.IsTorsionFree R M], m ≠ 0 → Function.Injective fun x => x • m

Defined in

Mathlib.Algebra.Module.Torsion.Free

Cited by

25 results in Mathlib

Foundations

Depth 22 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

RingAddCommGroupModuleIsCancelMulZeroModule.IsTorsionFree