Commit 2026-07-31 17:06 f4570dc2

View on Github →

chore(RingTheory/*): remove domain assumptions by generalizing from torsion free to faithful smul (#41379) This PR removes some IsDomain assumptions by generalizing Module.IsTorsionFree to FaithfulSMul. (As @SnirBroshi pointed out in the comments, this is not quite a generalization when the top ring is the zero ring, but this never arises in practice).

Estimated changes

Modified Mathlib/RingTheory/Conductor.lean

Modified Mathlib/RingTheory/Ideal/Maps.lean

modified theorem Ideal.map_ne_bot_of_ne_bot

Modified Mathlib/RingTheory/Ideal/Over.lean

modified theorem Ideal.ne_bot_of_mem_primesOver