Instances for HasEnoughRootsOfUnity #
We provide an instance for HasEnoughRootsOfUnity F n when F is an algebraically closed field
and n is not divisible by the characteristic. In particular, when F has characteristic zero,
this hold for all n ≠ 0.
TODO #
Add an instance HasEnoughRootsOfUnity Circle n for all n ≠ 0.
This is probably easiest via setting up an isomorphism
rootsOfUnity n Circle ≃* rootsOfUnity n ℂ.
instance
IsAlgClosed.hasEnoughRootsOfUnity
(F : Type u_1)
[Field F]
[IsAlgClosed F]
(n : ℕ)
[i : NeZero ↑n]
:
An algebraically closed field F satisfies HasEnoughRootsOfUnity F n for all n
that are not divisible by the characteristic of F.