mathlib

f3dd4ac6 - feat(group_theory/sylow): Injectivity of `sylow.subtype` (#16717)

feat(group_theory/sylow): Injectivity of `sylow.subtype` (#16717) `sylow.subtype` is injective if both Sylow subgroups are contained in the subgroup that you are restricting to. Co-authored-by: Thomas Browning <tb65536@users.noreply.github.com>