Theorem card_rootsOfUnity

Modification history

2024-12-30 19:50
Mathlib/RingTheory/RootsOfUnity/Basic.lean
chore: Replace `open scoped Classical` with `open scoped Classical in` or `classical` (#20325) …
Modified card_rootsOfUnityView on Github →
2023-06-07 12:41
Mathlib/RingTheory/RootsOfUnity/Basic.lean
feat: port RingTheory.RootsOfUnity.Basic (#4677)
Added card_rootsOfUnityView on Github →