instDifferentialAlgebraSubtypeMemIntermediateField_1

English

If B is a finite-dimensional intermediate field and K is a differential-algebra over F, then differentiation lifts through the inclusion map to B.

Русский

Если B — конечнодименсиональное промежуточное поле и K — дифференциальная алгебра над F, дифференциация переносится через вложение в B.

LaTeX

$$$\\text{DifferentialAlgebra } B K$$$

Lean4

instance [Differential K] [DifferentialAlgebra F K] (B : IntermediateField F K) [FiniteDimensional F B] :
    DifferentialAlgebra B K where
  deriv_algebraMap
    a := by
    change (B.val a)′ = B.val a′
    rw [algHom_deriv']
    exact Subtype.val_injective

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