Theorem NonUnitalSubring.closure_le_centralizer_centralizer

Modification history

2026-03-13 18:00
Mathlib/RingTheory/NonUnitalSubring/Basic.lean
feat: add `NonUnitalSubring.centralizer` (#36547) …
Added NonUnitalSubring.closure_le_centralizer_centralizerView on Github →