Theorem HasEnoughRootsOfUnity.natCard_rootsOfUnity

Modification history

2024-11-06 07:46
Mathlib/RingTheory/RootsOfUnity/EnoughRootsOfUnity.lean
feat(RingTheory/RootsOfUnity/EnoughRootsOfUnity): new file (#18681) …
Added HasEnoughRootsOfUnity.natCard_rootsOfUnityView on Github →