Theorem pow_gcd_card_eq_one_iff

Modification history

2026-07-15 16:59
Mathlib/GroupTheory/OrderOfElement.lean
chore: delete deprecated declarations to the end of 2025 (#41178) …
Deleted pow_gcd_card_eq_one_iffView on Github →
2025-12-12 08:03
Mathlib/GroupTheory/OrderOfElement.lean
feat: strengthen `pow_gcd_eq_one` (#32464) …
Modified pow_gcd_card_eq_one_iffView on Github →
2025-12-07 22:10
Mathlib/GroupTheory/OrderOfElement.lean
feat(Dynamics/PeriodicPts): some theorems for `Pi.map` in `Dynamics/PeriodicPts` analogous to those for `Prod.map` (#29530) …
Modified pow_gcd_card_eq_one_iffView on Github →
2023-02-22 16:34
Mathlib/GroupTheory/OrderOfElement.lean
feat: port GroupTheory.OrderOfElement (#2279)
Added pow_gcd_card_eq_one_iffView on Github →