English
An auxiliary construction that, given n and a polynomial f, produces a field extension and related algebraic data by iterating removals of factors.
Русский
Вспомогательное построение, которое при задании n и мером f строит конечное поле-расширение и связанные алгебраические данные через итеративное удаление множителей.
LaTeX
$$$\\text{SplittingFieldAuxAux}(n) : \\forall K\\,[\\text{Field }K], K[X] \\to \\Sigma (L) (\\text{Field }L) \\times \\text{Algebra }K L$$$
Lean4
/-- Auxiliary construction to a splitting field of a polynomial, which removes
`n` (arbitrarily-chosen) factors.
It constructs the type, proves that is a field and algebra over the base field.
Uses recursion on the degree.
-/
def SplittingFieldAuxAux (n : ℕ) : ∀ {K : Type u} [Field K], K[X] → Σ (L : Type u) (_ : Field L), Algebra K L :=
-- Porting note: added motive
Nat.recOn (motive := fun (_x : ℕ) =>
∀ {K : Type u} [_inst_4 : Field K], K[X] → Σ (L : Type u) (_ : Field L), Algebra K L) n
(fun {K} _ _ => ⟨K, inferInstance, inferInstance⟩) fun _ ih _ _ f =>
let ⟨L, fL, _⟩ := ih f.removeFactor
⟨L, fL, (RingHom.comp (algebraMap _ _) (AdjoinRoot.of f.factor)).toAlgebra⟩
