Mathlib v3 is deprecated. Go to Mathlib v4

Theorem sylow.mem_fixed_points_mul_left_cosets_iff_mem_normalizer

Modification history

2022-08-17 14:53
src/group_theory/sylow.lean
chore(group_theory/*): Fix lint (#16095) …
Modified sylow.mem_fixed_points_mul_left_cosets_iff_mem_normalizerView on Github →
2020-10-12 18:08
src/group_theory/sylow.lean
chore(*): update to Lean 3.21.0c (#4578) …
Modified sylow.mem_fixed_points_mul_left_cosets_iff_mem_normalizerView on Github →
2020-08-02 16:01
src/group_theory/sylow.lean
chore(group_theory/*): refactor quotient groups to use bundled subgroups (#3321)
Modified sylow.mem_fixed_points_mul_left_cosets_iff_mem_normalizerView on Github →
2019-01-14 14:48
group_theory/sylow.lean
feat(group_theory/sylow): first sylow theorem (closes #591)
Added sylow.mem_fixed_points_mul_left_cosets_iff_mem_normalizerView on Github →