Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-04-06 05:50 53128954

View on Github →

chore(group_theory/order_of_element): move some lemmas (#7031) I moved a few lemmas to group_theory.subgroup and to group_theory.coset and to data.finset.basic. Feel free to suggest different locations if they don't quite fit. This resolves #1563. Renamed card_trivial to subgroup.card_bot

Estimated changes

Modified docs/100.yaml

Modified src/data/finset/basic.lean

added theorem finset.mem_range_iff_mem_finset_range_of_mod_eq'

added theorem finset.mem_range_iff_mem_finset_range_of_mod_eq

Modified src/group_theory/coset.lean

added theorem subgroup.card_eq_card_quotient_mul_card_subgroup

added theorem subgroup.card_quotient_dvd_card

added theorem subgroup.card_subgroup_dvd_card

Modified src/group_theory/order_of_element.lean

deleted theorem card_eq_card_quotient_mul_card_subgroup

deleted theorem card_quotient_dvd_card

deleted theorem card_subgroup_dvd_card

deleted theorem card_trivial

deleted theorem finset.mem_range_iff_mem_finset_range_of_mod_eq'

deleted theorem finset.mem_range_iff_mem_finset_range_of_mod_eq

deleted theorem mem_normalizer_fintype

Modified src/group_theory/perm/sign.lean

Modified src/group_theory/subgroup.lean

added theorem add_subgroup.card_bot

added theorem subgroup.card_bot

added theorem subgroup.mem_normalizer_fintype

Modified src/group_theory/sylow.lean