Commit 2023-08-25 20:01 465dada7

View on Github →

feat: unit equivalences (#6526) Useful for Wedderburn's little theorem.

Estimated changes

Modified Mathlib/GroupTheory/GroupAction/ConjAct.lean

added def unitsCentralizerEquiv

Modified Mathlib/GroupTheory/Subgroup/Basic.lean

added def Subgroup.centerUnitsEquivUnitsCenter

Modified Mathlib/GroupTheory/Submonoid/Center.lean

added def unitsCenterToCenterUnits

added theorem unitsCenterToCenterUnits_injective