Theorem Subsemiring.le_centralizer_centralizer

Modification history

2024-06-04 06:29
Mathlib/Algebra/Ring/Subsemiring/Basic.lean
feat: The triple centralizer is equal to the centralizer (#13492) …
Added Subsemiring.le_centralizer_centralizerView on Github →