Commit 2022-10-26 07:42 179dcdea

View on Github →

refactor(group_theory/order_of_element): Remove fintype hypothesis from pow_coprime (#16989) This PR removes the [fintype G] hypothesis from pow_coprime (h : coprime (card G) n) : G ≃ G (the bijection given by the nth power map).

Estimated changes

Modified src/group_theory/order_of_element.lean

added theorem order_of_dvd_nat_card

added theorem pow_card_eq_one'

deleted def pow_coprime

modified theorem pow_coprime_inv

modified theorem pow_coprime_one

Modified src/group_theory/schur_zassenhaus.lean

modified theorem subgroup.eq_one_of_smul_eq_one

modified theorem subgroup.exists_smul_eq