English
If K is a finite-dimensional extension of F, then there exists a differential-algebra structure on K extending F.
Русский
Если K конечнодименсионально над F, то на K можно определить дифференциальную алгебру над F.
LaTeX
$$$\\text{DifferentialAlgebra } F K$$$
Lean4
/-- If `K` is a finite field extension of `F` then we can define a differential algebra on `K`, by
choosing a primitive element of `K`, `k` and then using the equivalence to `AdjoinRoot (minpoly k)`.
-/
@[reducible]
noncomputable def differentialFiniteDimensional [FiniteDimensional F K] : Differential K :=
let k := (Field.exists_primitive_element F K).choose
have h : F⟮k⟯ = ⊤ := (Field.exists_primitive_element F K).choose_spec
have : Fact (minpoly F k).Monic := ⟨minpoly.monic (IsAlgebraic.of_finite ..).isIntegral⟩
have : Fact (Irreducible (minpoly F k)) := ⟨minpoly.irreducible (IsAlgebraic.of_finite ..).isIntegral⟩
Differential.equiv
(IntermediateField.adjoinRootEquivAdjoin F (IsAlgebraic.of_finite F k).isIntegral |>.trans
(IntermediateField.equivOfEq h) |>.trans
IntermediateField.topEquiv).symm.toRingEquiv
