Commit 2024-12-31 11:45 62f34f74

View on Github →

feat(RingTheory): lemmas about annihilator (#20341)

Estimated changes

Modified Mathlib/RingTheory/Ideal/Maps.lean

added theorem Ideal.Module.annihilator_eq_bot

added theorem Ideal.Module.comap_annihilator