Theorem NonUnitalStarSubalgebra.comap_center_le_center

Modification history

2026-09-07 19:40
Mathlib/Algebra/Star/NonUnitalSubalgebra.lean
refactor: make several `NonUnitalStarSubalgebra(Hom)` definitions take a particular algebra homomorphism (#43377) …
Modified NonUnitalStarSubalgebra.comap_center_le_centerView on Github →
2026-08-18 12:48
Mathlib/Algebra/Star/NonUnitalSubalgebra.lean
feat(Algebra): `center` map lemmas (#42105) …
Added NonUnitalStarSubalgebra.comap_center_le_centerView on Github →