Theorem rootsOfUnity_one

Modification history

2024-11-04 08:35

Mathlib/RingTheory/RootsOfUnity/Basic.lean

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

Modified rootsOfUnity_one View on Github →

2024-02-19 15:34

Mathlib/RingTheory/RootsOfUnity/Basic.lean

feat(LinearAlgebra/Matrix): center of special linear group (#7826) …

Added rootsOfUnity_one View on Github →