Theorems · Definition · field theory

Differential.uniqueDifferentialAlgebraFiniteDimensional

{F : Type u_2} →
  [inst : Field F] →
    [inst_1 : Differential F] →
      [CharZero F] →
        {K : Type u_3} →
          [inst_3 : Field K] →
            [inst_4 : Algebra F K] → [FiniteDimensional F K] → Unique { _a // DifferentialAlgebra F K }

A finite extension of a differential field has a unique derivation which agrees with the one on the base field.

Defined in

Mathlib.FieldTheory.Differential.Basic

Cited by

0 results in Mathlib

Foundations

Depth 161 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

FieldDifferentialCharZeroFieldAlgebraFiniteDimensional