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

leanprover-community · Nov 11, 2024 · 006c0fc · 006c0fc
1 parent 21776d1
commit 006c0fc
Show file tree

Hide file tree

Showing 4 changed files with 24 additions and 12 deletions.
diff --git a/Mathlib/Topology/Algebra/Algebra.lean b/Mathlib/Topology/Algebra/Algebra.lean
@@ -555,8 +555,10 @@ theorem Subalgebra.topologicalClosure_minimal (s : Subalgebra R A) {t : Subalgeb
     (ht : IsClosed (t : Set A)) : s.topologicalClosure ≤ t :=
   closure_minimal h ht
 
-/-- If a subalgebra of a topological algebra is commutative, then so is its topological closure. -/
-def Subalgebra.commSemiringTopologicalClosure [T2Space A] (s : Subalgebra R A)
+/-- If a subalgebra of a topological algebra is commutative, then so is its topological closure.
+
+See note [reducible non-instances]. -/
+abbrev Subalgebra.commSemiringTopologicalClosure [T2Space A] (s : Subalgebra R A)
     (hs : ∀ x y : s, x * y = y * x) : CommSemiring s.topologicalClosure :=
   { s.topologicalClosure.toSemiring, s.toSubmonoid.commMonoidTopologicalClosure hs with }
 

diff --git a/Mathlib/Topology/Algebra/Group/Basic.lean b/Mathlib/Topology/Algebra/Group/Basic.lean
@@ -680,11 +680,15 @@ def Subgroup.connectedComponentOfOne (G : Type*) [TopologicalSpace G] [Group G]
   mul_mem' hg hh := mul_mem_connectedComponent_one hg hh
   inv_mem' hg := inv_mem_connectedComponent_one hg
 
-/-- If a subgroup of a topological group is commutative, then so is its topological closure. -/
+/-- If a subgroup of a topological group is commutative, then so is its topological closure.
+
+See note [reducible non-instances]. -/
 @[to_additive
   "If a subgroup of an additive topological group is commutative, then so is its
-  topological closure."]
-def Subgroup.commGroupTopologicalClosure [T2Space G] (s : Subgroup G)
+topological closure.
+
+See note [reducible non-instances]."]
+abbrev Subgroup.commGroupTopologicalClosure [T2Space G] (s : Subgroup G)
     (hs : ∀ x y : s, x * y = y * x) : CommGroup s.topologicalClosure :=
   { s.topologicalClosure.toGroup, s.toSubmonoid.commMonoidTopologicalClosure hs with }
 

diff --git a/Mathlib/Topology/Algebra/Monoid.lean b/Mathlib/Topology/Algebra/Monoid.lean
@@ -434,8 +434,10 @@ theorem Submonoid.topologicalClosure_minimal (s : Submonoid M) {t : Submonoid M}
 
 /-- If a submonoid of a topological monoid is commutative, then so is its topological closure. -/
 @[to_additive "If a submonoid of an additive topological monoid is commutative, then so is its
-topological closure."]
-def Submonoid.commMonoidTopologicalClosure [T2Space M] (s : Submonoid M)
+topological closure.
+
+See note [reducible non-instances]."]
+abbrev Submonoid.commMonoidTopologicalClosure [T2Space M] (s : Submonoid M)
     (hs : ∀ x y : s, x * y = y * x) : CommMonoid s.topologicalClosure :=
   { s.topologicalClosure.toMonoid with
     mul_comm :=

diff --git a/Mathlib/Topology/Algebra/Ring/Basic.lean b/Mathlib/Topology/Algebra/Ring/Basic.lean
@@ -115,8 +115,10 @@ theorem Subsemiring.topologicalClosure_minimal (s : Subsemiring α) {t : Subsemi
   closure_minimal h ht
 
 /-- If a subsemiring of a topological semiring is commutative, then so is its
-topological closure. -/
-def Subsemiring.commSemiringTopologicalClosure [T2Space α] (s : Subsemiring α)
+topological closure.
+
+See note [reducible non-instances]. -/
+abbrev Subsemiring.commSemiringTopologicalClosure [T2Space α] (s : Subsemiring α)
     (hs : ∀ x y : s, x * y = y * x) : CommSemiring s.topologicalClosure :=
   { s.topologicalClosure.toSemiring, s.toSubmonoid.commMonoidTopologicalClosure hs with }
 
@@ -250,9 +252,11 @@ theorem Subring.topologicalClosure_minimal (s : Subring α) {t : Subring α} (h
     (ht : IsClosed (t : Set α)) : s.topologicalClosure ≤ t :=
   closure_minimal h ht
 
-/-- If a subring of a topological ring is commutative, then so is its topological closure. -/
-def Subring.commRingTopologicalClosure [T2Space α] (s : Subring α) (hs : ∀ x y : s, x * y = y * x) :
-    CommRing s.topologicalClosure :=
+/-- If a subring of a topological ring is commutative, then so is its topological closure.
+
+See note [reducible non-instances]. -/
+abbrev Subring.commRingTopologicalClosure [T2Space α] (s : Subring α)
+    (hs : ∀ x y : s, x * y = y * x) : CommRing s.topologicalClosure :=
   { s.topologicalClosure.toRing, s.toSubmonoid.commMonoidTopologicalClosure hs with }
 
 end TopologicalSemiring