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 matchNat.card_subgroupPowers
)Submonoid.powers_subset
→Submonoid.powers_le
orderOf_dvd_card_univ
→orderOf_dvd_card
orderOf_subgroup
→Subgroup.orderOf
Subgroup.nonempty
→Subgroup.coe_nonempty