Theorem exists_prime_addEquiv_ZMod

Modification history

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