Commit 2023-01-27 15:48 a34afbb0

View on Github →

feat: port GroupTheory.Subgroup.Saturated (#1884)

Estimated changes

Modified Mathlib.lean

Created Mathlib/GroupTheory/Subgroup/Saturated.lean

added theorem AddSubgroup.ker_saturated

added def Subgroup.Saturated

added theorem Subgroup.saturated_iff_npow

added theorem Subgroup.saturated_iff_zpow