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.