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)
@[deprecated IsSepClosed.hasEnoughRootsOfUnity (since := "2025-06-22")]
theorem
IsAlgClosed.hasEnoughRootsOfUnity
(F : Type u_1)
[Field F]
(n : ℕ)
[NeZero ↑n]
[IsSepClosed F]
:
Alias of IsSepClosed.hasEnoughRootsOfUnity
.
A separably closed field F
satisfies HasEnoughRootsOfUnity F n
for all n
that are not divisible by the characteristic of F
.
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)