Commit 2024-01-08 12:05 8b2dcf6e

feat (RingTheory/Ideal/QuotientOperations) : remove commutativity assumption (#9495) This PR removes commutativity instances on the target of lift lemmas as well as some equivalences. It adds two short lemmas:

• RingHom.quotientKerEquivRangeS, a version of the first isomorphism theorem when the target is only a Semiring
• RingHom.ker_rangeSRestrict , a version of RingHom.ker_rangeRestrict when the target is only a Semiring.