SplittingFieldAux — Mathlib

English

For a polynomial f, SplittingFieldAux(n,f) is the underlying field part of the auxiliary splitting field constructed after removing n factors.

Русский

Для многочлена f и целого n, SplittingFieldAux(n,f) является полем-основой вспомогательного разворачивающего поля после удаления n множителей.

LaTeX

$$$\\text{SplittingFieldAux}(n,f) = \\pi_1(\\text{SplittingFieldAuxAux}(n,f))$$$

Lean4

/-- Auxiliary construction to a splitting field of a polynomial, which removes
`n` (arbitrarily-chosen) factors. It is the type constructed in `SplittingFieldAuxAux`.
-/
def SplittingFieldAux (n : ℕ) {K : Type u} [Field K] (f : K[X]) : Type u :=
  (SplittingFieldAuxAux n f).1

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