Commit 2022-05-31 09:47 8315ad02

View on Github →

refactor(group_theory/sylow): Move basic API earlier in the file (#14367) This PR moves some basic sylow API to earlier in the file, so that it can be used earlier.

Estimated changes

Modified src/group_theory/sylow.lean

modified theorem sylow.coe_comap_of_injective

modified theorem sylow.coe_comap_of_ker_is_p_group

modified theorem sylow.coe_subtype

modified def sylow.comap_of_injective

modified def sylow.comap_of_ker_is_p_group

modified def sylow.subtype