Instances for HasEnoughRootsOfUnity #
We provide an instance for HasEnoughRootsOfUnity F n when F is a separably closed field
and n is not divisible by the characteristic. In particular, when F has characteristic zero,
this hold for all n ≠ 0.
instance IsSepClosed.hasEnoughRootsOfUnity (F : Type u_1) [Field F] (n : ℕ) [NeZero ↑n] [IsSepClosed F] :
A separably closed field F satisfies HasEnoughRootsOfUnity F n for all n
that are not divisible by the characteristic of F.
instance IsSepClosed.hasEnoughRootsOfUnity_pow (F : Type u_1) [Field F] (n k : ℕ) [NeZero ↑n] [IsSepClosed F] :
HasEnoughRootsOfUnity F (n ^ k)
instance AlgebraicClosure.hasEnoughRootsOfUnity_pow (F : Type u_1) [Field F] (n k : ℕ) [NeZero ↑n] :
HasEnoughRootsOfUnity (AlgebraicClosure F) (n ^ k)
instance SeparableClosure.hasEnoughRootsOfUnity_pow (F : Type u_1) [Field F] (n k : ℕ) [NeZero ↑n] :
HasEnoughRootsOfUnity (SeparableClosure F) (n ^ k)