Commit 2026-08-18 12:48 7ec3906d

View on Github →

feat(Algebra): center map lemmas (#42105) Plumb lemmas showing surjective homs/isos map centers to centers throughout the algebra hierarchy.

Estimated changes

added theorem Set.image_center_eq
added theorem Subring.map_center_eq
modified def Subgroup.centerCongr
added theorem Subgroup.map_center_eq