mathlib3
8315ad02 - refactor(group_theory/sylow): Move basic API earlier in the file (#14367)

Commit

3 years ago

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.

Author

tb65536

Parents

111ce5b8

mathlib3 8315ad02 - refactor(group_theory/sylow): Move basic API earlier in the file (#14367)

mathlib3
8315ad02 - refactor(group_theory/sylow): Move basic API earlier in the file (#14367)