Commit 2023-11-14 18:13 ee3bd06d

View on Github →

feat: Order of elements of a subgroup (#8385) The cardinality of a subgroup is greater than the order of any of its elements. Rename

  • order_eq_card_zpowers → Fintype.card_zpowers
  • order_eq_card_zpowers' → Nat.card_zpowers (and turn it around to match Nat.card_subgroupPowers)
  • Submonoid.powers_subset → Submonoid.powers_le
  • orderOf_dvd_card_univ → orderOf_dvd_card
  • orderOf_subgroup → Subgroup.orderOf
  • Subgroup.nonempty → Subgroup.coe_nonempty

Estimated changes

added theorem Nat.card_zpowers
added theorem finite_zpowers
added theorem infinite_zpowers
deleted theorem order_eq_card_zpowers'
added theorem Fintype.card_zpowers
added theorem Subgroup.orderOf_coe
added theorem Subgroup.orderOf_mk
added theorem orderOf_dvd_card
deleted theorem orderOf_dvd_card_univ
added theorem orderOf_dvd_natCard
deleted theorem orderOf_dvd_nat_card
deleted theorem orderOf_eq_card_zpowers
deleted theorem orderOf_subgroup
added theorem Subgroup.coe_nonempty
deleted theorem Subgroup.nonempty
added theorem Submonoid.powers_le
modified theorem Submonoid.powers_one
deleted theorem Submonoid.powers_subset