Commit 2023-01-04 10:02 534caaeb

View on Github →

feat: port GroupTheory.Submonoid.Centralizer (#1324)

Estimated changes

Modified Mathlib.lean

Created Mathlib/GroupTheory/Submonoid/Centralizer.lean

added theorem AddSubmonoid.centralizer_toAddSubsemigroup

added def Submonoid.centralizer

added theorem Submonoid.centralizer_le

added theorem Submonoid.centralizer_toSubsemigroup

added theorem Submonoid.centralizer_univ

added theorem Submonoid.coe_centralizer

added theorem Submonoid.mem_centralizer_iff