hasEnoughRootsOfUnity_pow — Mathlib

English

HasEnoughRootsOfUnity holds for n^k in AlgebraicClosure F for all k.

Русский

В AlgebraicClosure F существует корни единства порядка n^k для всех k.

LaTeX

$$$\text{HasEnoughRootsOfUnity} (\mathrm{AlgClosed}(F)) (n^k)$$$

Lean4

instance hasEnoughRootsOfUnity_pow : HasEnoughRootsOfUnity (AlgebraicClosure F) (n ^ k) :=
  have : NeZero (n : AlgebraicClosure F) := ‹NeZero (n : F)›.of_injective (algebraMap F (AlgebraicClosure F)).injective
  inferInstance

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