English
If K is finite-dimensional over F, then K has a differential-algebra structure over F; in particular, differential-algebraic machinery transfers to K.
Русский
Если K конечнодименсионально над F, то K имеет дифференциальную алгебраическую структуру над F; следовательно, применимы дифференциально-алгебраические техники.
LaTeX
$$$\\text{DifferentialAlgebra } F K$$$
Lean4
theorem differentialAlgebraFiniteDimensional [FiniteDimensional F K] :
letI := differentialFiniteDimensional F K
DifferentialAlgebra F K :=
by
let k := (Field.exists_primitive_element F K).choose
haveI h : F⟮k⟯ = ⊤ := (Field.exists_primitive_element F K).choose_spec
haveI : Fact (minpoly F k).Monic := ⟨minpoly.monic (IsAlgebraic.of_finite ..).isIntegral⟩
haveI : Fact (Irreducible (minpoly F k)) := ⟨minpoly.irreducible (IsAlgebraic.of_finite ..).isIntegral⟩
apply DifferentialAlgebra.equiv
