Commit 2023-06-10 14:53 b0a21674

View on Github →

chore: port leanprover-community/mathlib#18861 (#4896) I forgot to put some required to_additives in Lean3, I am currently backporting this change in leanprover-community/mathlib#19168.

Estimated changes

Modified Mathlib/Algebra/Algebra/Subalgebra/Basic.lean

added theorem Subalgebra.center_le_centralizer

added theorem Subalgebra.centralizer_eq_top_iff_subset

Modified Mathlib/GroupTheory/Subgroup/Basic.lean

added theorem Subgroup.center_le_centralizer

added theorem Subgroup.centralizer_eq_top_iff_subset

Modified Mathlib/GroupTheory/Submonoid/Centralizer.lean

added theorem Submonoid.center_le_centralizer

added theorem Submonoid.centralizer_eq_top_iff_subset

Modified Mathlib/GroupTheory/Subsemigroup/Centralizer.lean

added theorem Set.center_subset_centralizer

added theorem Set.centralizer_eq_top_iff_subset

added theorem Subsemigroup.center_le_centralizer

added theorem Subsemigroup.centralizer_eq_top_iff_subset

Modified Mathlib/RingTheory/NonUnitalSubsemiring/Basic.lean

added theorem NonUnitalSubsemiring.center_le_centralizer

added theorem NonUnitalSubsemiring.centralizer_eq_top_iff_subset

Modified Mathlib/RingTheory/Subring/Basic.lean

added theorem Subring.center_le_centralizer

added def Subring.centralizer

added theorem Subring.centralizer_eq_top_iff_subset

added theorem Subring.centralizer_le

added theorem Subring.centralizer_toSubmonoid

added theorem Subring.centralizer_toSubsemiring

added theorem Subring.centralizer_univ

added theorem Subring.coe_centralizer

added theorem Subring.mem_centralizer_iff

Modified Mathlib/RingTheory/Subsemiring/Basic.lean

added theorem Subsemiring.center_le_centralizer

added theorem Subsemiring.centralizer_eq_top_iff_subset