Commit 2024-02-22 22:58 e9e590d6
View on Github →feat: generalize direct sum results to avoid negation (#10828)
Three files are modified, where the hypotheses are relaxed from Ring or CommRing to Semiring or CommSemiring, and AddCommGroup to AddCommMonoid.
Besides this, no definition is changed, and for one proof in RingTheory.Flat.Basic, I needed to add an instance (letI…) in the proof.
(Everything pertains to direct sums of modules.)