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)