Def rootsOfUnity

Modification history

2024-11-04 08:35

Mathlib/RingTheory/RootsOfUnity/Basic.lean

chore: refactor roots of unity to avoid PNat (#18516) …

Modified rootsOfUnity View on Github →

2023-08-10 19:52

Mathlib/RingTheory/RootsOfUnity/Basic.lean

chore: banish `Type _` and `Sort _` (#6499) …

Modified rootsOfUnity View on Github →

2023-06-07 12:41

Mathlib/RingTheory/RootsOfUnity/Basic.lean

feat: port RingTheory.RootsOfUnity.Basic (#4677)

Added rootsOfUnity View on Github →