mathlib
2f18952b - feat(group_theory/p_group): If `p ∤ n`, then the `n`th power map is a bijection (#17193)

Commit

3 years ago

feat(group_theory/p_group): If `p ∤ n`, then the `n`th power map is a bijection (#17193) This PR proves that if `p ∤ n`, then the `n`th power map is a bijection.

Author

tb65536

Parents

f8393c90

mathlib 2f18952b - feat(group_theory/p_group): If `p ∤ n`, then the `n`th power map is a bijection (#17193)

mathlib
2f18952b - feat(group_theory/p_group): If `p ∤ n`, then the `n`th power map is a bijection (#17193)