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.

Estimated changes