Commit 2024-10-28 23:09 d57b21ae
View on Github →refactor(RingTheory/Ideal/Pointwise): Generalize to semirings (#18355)
This PR generalizes much of RingTheory/Ideal/Pointwise
to semirings. I also moved a couple lemmas from the Group
section to the Monoid
section, and added a lemma to RingTheory/Ideal/Over
.