Commit 2026-03-13 18:00 63057c9c

View on Github →

feat: add NonUnitalSubring.centralizer (#36547) We have this for all the other variants (NonUnitalSemiring, Subsemiring, Subring), but this one was missing. The lemmas are copy-pasted from their counterparts.

Estimated changes

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

added theorem Subring.centralizer_toNonUnitalSubring

Modified Mathlib/RingTheory/NonUnitalSubring/Basic.lean

added theorem NonUnitalSubring.center_le_centralizer

added def NonUnitalSubring.centralizer

added theorem NonUnitalSubring.centralizer_eq_top_iff_subset

added theorem NonUnitalSubring.centralizer_le

added theorem NonUnitalSubring.centralizer_toNonUnitalSubsemiring

added theorem NonUnitalSubring.centralizer_univ

added theorem NonUnitalSubring.closure_le_centralizer_centralizer

added theorem NonUnitalSubring.coe_centralizer

added theorem NonUnitalSubring.mem_centralizer_iff