Theorem Module.support_of_noZeroSMulDivisors

Modification history

2026-01-13 19:40

Mathlib/RingTheory/Support.lean

chore(Algebra): replace `NoZeroSMulDivisors` with `Module.IsTorsionFree` wlog (#30563) …

Modified Module.support_of_noZeroSMulDivisors View on Github →

2024-07-22 15:39

Mathlib/RingTheory/Support.lean

feat(RingTheory/Support): Define support of a module (#14507) …

Added Module.support_of_noZeroSMulDivisors View on Github →