chore: port leanprover-community/mathlib#18861 (#4896)

I forgot to put some required `to_additive`s in Lean3, I am currently backporting this change in leanprover-community/mathlib#19168.



Co-authored-by: Eric Rodriguez <37984851+ericrbg@users.noreply.github.com>

Mathlib/Algebra/Algebra/Subalgebra/Basic.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kenny Lau, Yury Kudryashov
 
 ! This file was ported from Lean 3 source module algebra.algebra.subalgebra.basic
-! leanprover-community/mathlib commit 8130e5155d637db35907c272de9aec9dc851c03a
+! leanprover-community/mathlib commit b915e9392ecb2a861e1e766f0e1df6ac481188ca
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -1403,10 +1403,19 @@ theorem mem_centralizer_iff {s : Set A} {z : A} : z ∈ centralizer R s ↔ ∀
   Iff.rfl
 #align subalgebra.mem_centralizer_iff Subalgebra.mem_centralizer_iff
 
+theorem center_le_centralizer (s) : center R A ≤ centralizer R s :=
+  s.center_subset_centralizer
+#align subalgebra.center_le_centralizer Subalgebra.center_le_centralizer
+
 theorem centralizer_le (s t : Set A) (h : s ⊆ t) : centralizer R t ≤ centralizer R s :=
   Set.centralizer_subset h
 #align subalgebra.centralizer_le Subalgebra.centralizer_le
 
+@[simp]
+theorem centralizer_eq_top_iff_subset {s : Set A} : centralizer R s = ⊤ ↔ s ⊆ center R A :=
+  SetLike.ext'_iff.trans Set.centralizer_eq_top_iff_subset
+#align subalgebra.centralizer_eq_top_iff_subset Subalgebra.centralizer_eq_top_iff_subset
+
 @[simp]
 theorem centralizer_univ : centralizer R Set.univ = center R A :=
   SetLike.ext' (Set.centralizer_univ A)

Mathlib/GroupTheory/Subgroup/Basic.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kexing Ying
 
 ! This file was ported from Lean 3 source module group_theory.subgroup.basic
-! leanprover-community/mathlib commit 6b60020790e39e77bfd633ba3d5562ff82e52c79
+! leanprover-community/mathlib commit cc67cd75b4e54191e13c2e8d722289a89e67e4fa
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -2301,12 +2301,24 @@ theorem le_centralizer_iff : H ≤ K.centralizer ↔ K ≤ H.centralizer :=
 #align subgroup.le_centralizer_iff Subgroup.le_centralizer_iff
 #align add_subgroup.le_centralizer_iff AddSubgroup.le_centralizer_iff
 
+@[to_additive]
+theorem center_le_centralizer (s) : center G ≤ centralizer s :=
+  Set.center_subset_centralizer (s : Set G)
+#align subgroup.center_le_centralizer Subgroup.center_le_centralizer
+#align add_subgroup.center_le_centralizer AddSubgroup.center_le_centralizer
+
 @[to_additive]
 theorem centralizer_le (h : H ≤ K) : centralizer K ≤ centralizer H :=
   Submonoid.centralizer_le h
 #align subgroup.centralizer_le Subgroup.centralizer_le
 #align add_subgroup.centralizer_le AddSubgroup.centralizer_le
 
+@[to_additive (attr := simp)]
+theorem centralizer_eq_top_iff_subset {s} : centralizer s = ⊤ ↔ s ≤ center G :=
+  SetLike.ext'_iff.trans Set.centralizer_eq_top_iff_subset
+#align subgroup.centralizer_eq_top_iff_subset Subgroup.centralizer_eq_top_iff_subset
+#align add_subgroup.centralizer_eq_top_iff_subset AddSubgroup.centralizer_eq_top_iff_subset
+
 @[to_additive]
 instance Centralizer.characteristic [hH : H.Characteristic] :
     H.centralizer.Characteristic := by

Mathlib/GroupTheory/Submonoid/Centralizer.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Thomas Browning
 
 ! This file was ported from Lean 3 source module group_theory.submonoid.centralizer
-! leanprover-community/mathlib commit 44b58b42794e5abe2bf86397c38e26b587e07e59
+! leanprover-community/mathlib commit cc67cd75b4e54191e13c2e8d722289a89e67e4fa
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -66,6 +66,12 @@ theorem mem_centralizer_iff {z : M} : z ∈ centralizer S ↔ ∀ g ∈ S, g * z
 #align submonoid.mem_centralizer_iff Submonoid.mem_centralizer_iff
 #align add_submonoid.mem_centralizer_iff AddSubmonoid.mem_centralizer_iff
 
+@[to_additive]
+theorem center_le_centralizer (s) : center M ≤ centralizer s :=
+  s.center_subset_centralizer
+#align submonoid.center_le_centralizer Submonoid.center_le_centralizer
+#align add_submonoid.center_le_centralizer AddSubmonoid.center_le_centralizer
+
 @[to_additive]
 instance decidableMemCentralizer (a) [Decidable <| ∀ b ∈ S, b * a = a * b] :
     Decidable (a ∈ centralizer S) :=
@@ -79,6 +85,12 @@ theorem centralizer_le (h : S ⊆ T) : centralizer T ≤ centralizer S :=
 #align submonoid.centralizer_le Submonoid.centralizer_le
 #align add_submonoid.centralizer_le AddSubmonoid.centralizer_le
 
+@[to_additive (attr := simp)]
+theorem centralizer_eq_top_iff_subset {s : Set M} : centralizer s = ⊤ ↔ s ⊆ center M :=
+  SetLike.ext'_iff.trans Set.centralizer_eq_top_iff_subset
+#align submonoid.centralizer_eq_top_iff_subset Submonoid.centralizer_eq_top_iff_subset
+#align add_submonoid.centralizer_eq_top_iff_subset AddSubmonoid.centralizer_eq_top_iff_subset
+
 variable (M)
 
 @[to_additive (attr := simp)]

Mathlib/GroupTheory/Subsemigroup/Centralizer.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Thomas Browning, Jireh Loreaux
 
 ! This file was ported from Lean 3 source module group_theory.subsemigroup.centralizer
-! leanprover-community/mathlib commit ffc3730d545623aedf5d5bd46a3153cbf41f6c2c
+! leanprover-community/mathlib commit cc67cd75b4e54191e13c2e8d722289a89e67e4fa
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -41,6 +41,8 @@ def centralizer [Mul M] : Set M :=
 
 variable {S}
 
+-- TODO: this additive naming in this section does not conform to the
+-- naming convention. This will be fixed soon.
 @[to_additive mem_add_centralizer]
 theorem mem_centralizer_iff [Mul M] {c : M} : c ∈ centralizer S ↔ ∀ m ∈ S, m * c = c * m :=
   Iff.rfl
@@ -122,6 +124,19 @@ theorem centralizer_subset [Mul M] (h : S ⊆ T) : centralizer T ⊆ centralizer
 #align set.centralizer_subset Set.centralizer_subset
 #align set.add_centralizer_subset Set.add_centralizer_subset
 
+@[to_additive addCenter_subset_addCentralizer]
+theorem center_subset_centralizer [Mul M] (S : Set M) : Set.center M ⊆ S.centralizer :=
+  fun _ hx m _ => hx m
+#align set.center_subset_centralizer Set.center_subset_centralizer
+#align set.add_center_subset_add_centralizer Set.addCenter_subset_addCentralizer
+
+@[to_additive (attr := simp) addCentralizer_eq_top_iff_subset]
+theorem centralizer_eq_top_iff_subset {s : Set M} [Mul M] :
+    centralizer s = Set.univ ↔ s ⊆ center M :=
+  eq_top_iff.trans <| ⟨fun h _ hx _ => (h trivial _ hx).symm, fun h x _ _ hm => (h hm x).symm⟩
+#align set.centralizer_eq_top_iff_subset Set.centralizer_eq_top_iff_subset
+#align set.add_centralizer_eq_top_iff_subset Set.addCentralizer_eq_top_iff_subset
+
 variable (M)
 
 @[to_additive (attr := simp) add_centralizer_univ]
@@ -175,12 +190,24 @@ instance decidableMemCentralizer (a) [Decidable <| ∀ b ∈ S, b * a = a * b] :
 #align subsemigroup.decidable_mem_centralizer Subsemigroup.decidableMemCentralizer
 #align add_subsemigroup.decidable_mem_centralizer AddSubsemigroup.decidableMemCentralizer
 
+@[to_additive]
+theorem center_le_centralizer (S) : center M ≤ centralizer S :=
+  S.center_subset_centralizer
+#align subsemigroup.center_le_centralizer Subsemigroup.center_le_centralizer
+#align add_subsemigroup.center_le_centralizer AddSubsemigroup.center_le_centralizer
+
 @[to_additive]
 theorem centralizer_le (h : S ⊆ T) : centralizer T ≤ centralizer S :=
   Set.centralizer_subset h
 #align subsemigroup.centralizer_le Subsemigroup.centralizer_le
 #align add_subsemigroup.centralizer_le AddSubsemigroup.centralizer_le
 
+@[to_additive (attr := simp)]
+theorem centralizer_eq_top_iff_subset {s : Set M} : centralizer s = ⊤ ↔ s ⊆ center M :=
+  SetLike.ext'_iff.trans Set.centralizer_eq_top_iff_subset
+#align subsemigroup.centralizer_eq_top_iff_subset Subsemigroup.centralizer_eq_top_iff_subset
+#align add_subsemigroup.centralizer_eq_top_iff_subset AddSubsemigroup.centralizer_eq_top_iff_subset
+
 variable (M)
 @[to_additive (attr := simp)]
 theorem centralizer_univ : centralizer Set.univ = center M :=

Mathlib/RingTheory/NonUnitalSubsemiring/Basic.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jireh Loreaux
 
 ! This file was ported from Lean 3 source module ring_theory.non_unital_subsemiring.basic
-! leanprover-community/mathlib commit feb99064803fd3108e37c18b0f77d0a8344677a3
+! leanprover-community/mathlib commit b915e9392ecb2a861e1e766f0e1df6ac481188ca
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -532,11 +532,21 @@ theorem mem_centralizer_iff {R} [NonUnitalSemiring R] {s : Set R} {z : R} :
   Iff.rfl
 #align non_unital_subsemiring.mem_centralizer_iff NonUnitalSubsemiring.mem_centralizer_iff
 
+theorem center_le_centralizer {R} [NonUnitalSemiring R] (s) : center R ≤ centralizer s :=
+  s.center_subset_centralizer
+#align non_unital_subsemiring.center_le_centralizer NonUnitalSubsemiring.center_le_centralizer
+
 theorem centralizer_le {R} [NonUnitalSemiring R] (s t : Set R) (h : s ⊆ t) :
     centralizer t ≤ centralizer s :=
   Set.centralizer_subset h
 #align non_unital_subsemiring.centralizer_le NonUnitalSubsemiring.centralizer_le
 
+@[simp]
+theorem centralizer_eq_top_iff_subset {R} [NonUnitalSemiring R] {s : Set R} :
+    centralizer s = ⊤ ↔ s ⊆ center R :=
+  SetLike.ext'_iff.trans Set.centralizer_eq_top_iff_subset
+#align non_unital_subsemiring.centralizer_eq_top_iff_subset NonUnitalSubsemiring.centralizer_eq_top_iff_subset
+
 @[simp]
 theorem centralizer_univ {R} [NonUnitalSemiring R] : centralizer Set.univ = center R :=
   SetLike.ext' (Set.centralizer_univ R)

Mathlib/RingTheory/Subring/Basic.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Ashvni Narayanan
 
 ! This file was ported from Lean 3 source module ring_theory.subring.basic
-! leanprover-community/mathlib commit feb99064803fd3108e37c18b0f77d0a8344677a3
+! leanprover-community/mathlib commit b915e9392ecb2a861e1e766f0e1df6ac481188ca
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -840,6 +840,52 @@ theorem center.coe_div (a b : center K) : ((a / b : center K) : K) = (a : K) / (
 
 end DivisionRing
 
+section Centralizer
+
+/-- The centralizer of a set inside a ring as a `Subring`. -/
+def centralizer (s : Set R) : Subring R :=
+  { Subsemiring.centralizer s with neg_mem' := Set.neg_mem_centralizer }
+#align subring.centralizer Subring.centralizer
+
+@[simp, norm_cast]
+theorem coe_centralizer (s : Set R) : (centralizer s : Set R) = s.centralizer :=
+  rfl
+#align subring.coe_centralizer Subring.coe_centralizer
+
+theorem centralizer_toSubmonoid (s : Set R) :
+    (centralizer s).toSubmonoid = Submonoid.centralizer s :=
+  rfl
+#align subring.centralizer_to_submonoid Subring.centralizer_toSubmonoid
+
+theorem centralizer_toSubsemiring (s : Set R) :
+    (centralizer s).toSubsemiring = Subsemiring.centralizer s :=
+  rfl
+#align subring.centralizer_to_subsemiring Subring.centralizer_toSubsemiring
+
+theorem mem_centralizer_iff {s : Set R} {z : R} : z ∈ centralizer s ↔ ∀ g ∈ s, g * z = z * g :=
+  Iff.rfl
+#align subring.mem_centralizer_iff Subring.mem_centralizer_iff
+
+theorem center_le_centralizer (s) : center R ≤ centralizer s :=
+  s.center_subset_centralizer
+#align subring.center_le_centralizer Subring.center_le_centralizer
+
+theorem centralizer_le (s t : Set R) (h : s ⊆ t) : centralizer t ≤ centralizer s :=
+  Set.centralizer_subset h
+#align subring.centralizer_le Subring.centralizer_le
+
+@[simp]
+theorem centralizer_eq_top_iff_subset {s : Set R} : centralizer s = ⊤ ↔ s ⊆ center R :=
+  SetLike.ext'_iff.trans Set.centralizer_eq_top_iff_subset
+#align subring.centralizer_eq_top_iff_subset Subring.centralizer_eq_top_iff_subset
+
+@[simp]
+theorem centralizer_univ : centralizer Set.univ = center R :=
+  SetLike.ext' (Set.centralizer_univ R)
+#align subring.centralizer_univ Subring.centralizer_univ
+
+end Centralizer
+
 /-! ## subring closure of a subset -/
 
 

Mathlib/RingTheory/Subsemiring/Basic.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yury Kudryashov
 
 ! This file was ported from Lean 3 source module ring_theory.subsemiring.basic
-! leanprover-community/mathlib commit feb99064803fd3108e37c18b0f77d0a8344677a3
+! leanprover-community/mathlib commit b915e9392ecb2a861e1e766f0e1df6ac481188ca
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -772,10 +772,20 @@ theorem mem_centralizer_iff {R} [Semiring R] {s : Set R} {z : R} :
   Iff.rfl
 #align subsemiring.mem_centralizer_iff Subsemiring.mem_centralizer_iff
 
+theorem center_le_centralizer {R} [Semiring R] (s) : center R ≤ centralizer s :=
+  s.center_subset_centralizer
+#align subsemiring.center_le_centralizer Subsemiring.center_le_centralizer
+
 theorem centralizer_le {R} [Semiring R] (s t : Set R) (h : s ⊆ t) : centralizer t ≤ centralizer s :=
   Set.centralizer_subset h
 #align subsemiring.centralizer_le Subsemiring.centralizer_le
 
+@[simp]
+theorem centralizer_eq_top_iff_subset {R} [Semiring R] {s : Set R} :
+    centralizer s = ⊤ ↔ s ⊆ center R :=
+  SetLike.ext'_iff.trans Set.centralizer_eq_top_iff_subset
+#align subsemiring.centralizer_eq_top_iff_subset Subsemiring.centralizer_eq_top_iff_subset
+
 @[simp]
 theorem centralizer_univ {R} [Semiring R] : centralizer Set.univ = center R :=
   SetLike.ext' (Set.centralizer_univ R)