hasEnoughRootsOfUnity — Mathlib

English

The SeparableClosure of F has HasEnoughRootsOfUnity for n.

Русский

Разделимо замкнутое замыкание SeparableClosure F имеет HasEnoughRootsOfUnity для n.

LaTeX

$$$\HasEnoughRootsOfUnity (\mathrm{SeparableClosure}(F))\ n$$$

Lean4

instance hasEnoughRootsOfUnity : HasEnoughRootsOfUnity (SeparableClosure F) n :=
  have : NeZero (n : SeparableClosure F) := ‹NeZero (n : F)›.of_injective (algebraMap F (SeparableClosure F)).injective
  inferInstance

Похожие утверждения