Theorem mem_zpowers_zpow_iff

Modification history

2026-01-08 08:52
Mathlib/GroupTheory/OrderOfElement.lean
feat(GroupTheory/SpecificGroups/Cyclic): generalize the proof of prime_card by not assuming Finite (#32152) …
Added mem_zpowers_zpow_iffView on Github →