Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-08-09 15:47 f3b70e4a

View on Github →

feat(group_theory/subgroup): saturated subgroups (#8137) From LTE

Estimated changes

Modified src/group_theory/subgroup.lean

added theorem add_subgroup.ker_saturated

added def subgroup.saturated

added theorem subgroup.saturated_iff_gpow

added theorem subgroup.saturated_iff_npow