Commit 2026-04-01 17:01 3bd2603b

View on Github →

chore: remove double instance on CommRing (SeparationQuotient α) (#37481) We had two different instances giving CommRing (SeparationQuotient α), defined differently and independently (and non-defeq). This PR removes one of them.

Estimated changes

Modified Mathlib/Topology/Algebra/SeparationQuotient/Basic.lean

Modified Mathlib/Topology/Algebra/UniformRing.lean

modified def UniformSpace.sepQuotHomeomorphRingQuot