Theorem Ideal.map_ne_bot_of_ne_bot

Modification history

2026-07-31 17:06
Mathlib/RingTheory/Ideal/Maps.lean
chore(RingTheory/*): remove domain assumptions by generalizing from torsion free to faithful smul (#41379) …
Modified Ideal.map_ne_bot_of_ne_botView on Github →
2026-01-13 19:40
Mathlib/RingTheory/Ideal/Maps.lean
chore(Algebra): replace `NoZeroSMulDivisors` with `Module.IsTorsionFree` wlog (#30563) …
Modified Ideal.map_ne_bot_of_ne_botView on Github →
2025-03-01 19:47
Mathlib/RingTheory/Ideal/Maps.lean
chore: make commands start at the start of a line (#22441) …
Added Ideal.map_ne_bot_of_ne_botView on Github →