English
A separably closed field F has enough roots of unity for all n not divisible by the characteristic of F.
Русский
Разделимо замкнутое поле F имеет достаточно корней единства для всех n, не делящих характеристику F.
LaTeX
$$$\forall n\in\mathbb{N},\ \gcd(n,\mathrm{char}(F)) = 1 \Rightarrow \HasEnoughRootsOfUnity F\ n$$$
Lean4
/-- A separably closed field `F` satisfies `HasEnoughRootsOfUnity F n` for all `n`
that are not divisible by the characteristic of `F`. -/
instance hasEnoughRootsOfUnity : HasEnoughRootsOfUnity F n
where
prim := by
have : NeZero n := .of_neZero_natCast F
have := isCyclotomicExtension { n } F fun _ h _ ↦ Set.mem_singleton_iff.mp h ▸ ‹NeZero (n : F)›
exact IsCyclotomicExtension.exists_isPrimitiveRoot (S := { n }) F _ rfl (NeZero.ne _)
cyc :=
have : NeZero n := .of_neZero_natCast F
rootsOfUnity.isCyclic F n
