Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-01-30 15:41 97f61dfd

View on Github →

feat(group_theory/sylow): preimages of sylow groups (#11722)

Estimated changes

Modified src/group_theory/sylow.lean

added theorem sylow.coe_comap_of_injective

added theorem sylow.coe_comap_of_ker_is_p_group

added theorem sylow.coe_subtype

added def sylow.comap_of_injective

added def sylow.comap_of_ker_is_p_group

added def sylow.subtype