Theorem Subalgebra.le_centralizer_centralizer

Modification history

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