Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-12-20 09:31 1854dd93

View on Github →

feat(group_theory/order_of_element): lemmas about card of subgroups and normalizer (#545)

Estimated changes

Modified group_theory/order_of_element.lean

added theorem card_eq_card_quotient_mul_card_subgroup

added theorem card_quotient_dvd_card

added theorem card_subgroup_dvd_card

added theorem card_trivial

added theorem conj_inj

added theorem mem_normalizer_fintype

added theorem order_of_eq_one_iff

added theorem order_of_one

Modified group_theory/subgroup.lean

modified def gmultiples

modified def gpowers

added def is_subgroup.normalizer

added theorem is_subgroup.subset_normalizer