Commit 2024-11-11 03:06 006c0fc2

View on Github →

chore: change comm*TopologicalClosure from def to abbrev (#18766)

Estimated changes

Modified Mathlib/Topology/Algebra/Algebra.lean

deleted def Subalgebra.commSemiringTopologicalClosure

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

deleted def Subgroup.commGroupTopologicalClosure

Modified Mathlib/Topology/Algebra/Monoid.lean

deleted def Submonoid.commMonoidTopologicalClosure

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

deleted def Subring.commRingTopologicalClosure

deleted def Subsemiring.commSemiringTopologicalClosure