The formal derivative on a rational function field and its constant field.

noncomputable def CCDN.rationalDerivativeFraction {K : Type u_1} [Field K] (p q : Polynomial K) : RatFunc K

The quotient-rule derivative (p' * q - p * q') / q ^ 2 of the fraction p / q.

Equations

• One or more equations did not get rendered due to their size.

theorem CCDN.rationalDerivativeFraction_mul {K : Type u_1} [Field K] {p q a : Polynomial K} (hq : q ≠ 0) (ha : a ≠ 0) : rationalDerivativeFraction (a * p) (a * q) = rationalDerivativeFraction p q

The quotient-rule derivative of a fraction is unchanged by multiplying its numerator and denominator by the same nonzero polynomial.

noncomputable def CCDN.rationalDerivative {K : Type u_1} [Field K] (x : RatFunc K) : RatFunc K

Formal rational differentiation, well-defined under changing fractions.

Equations

• CCDN.rationalDerivative x = x.liftOn' CCDN.rationalDerivativeFraction ⋯

theorem CCDN.rationalDerivative_polynomial {K : Type u_1} [Field K] (p : Polynomial K) : rationalDerivative ((algebraMap (Polynomial K) (RatFunc K)) p) = (algebraMap (Polynomial K) (RatFunc K)) (Polynomial.derivative p)

The formal rational derivative of a polynomial is its ordinary derivative.

theorem CCDN.rationalDerivative_add {K : Type u_1} [Field K] (x y : RatFunc K) : rationalDerivative (x + y) = rationalDerivative x + rationalDerivative y

The formal rational derivative is additive.

theorem CCDN.rationalDerivative_mul {K : Type u_1} [Field K] (x y : RatFunc K) : rationalDerivative (x * y) = x * rationalDerivative y + y * rationalDerivative x

The formal rational derivative satisfies the Leibniz rule.

noncomputable def CCDN.rationalDerivation (K : Type u_2) [Field K] : Derivation K (RatFunc K) (RatFunc K)

Rational formal differentiation as a derivation over the coefficient field.

Equations

• CCDN.rationalDerivation K = { toFun := CCDN.rationalDerivative, map_add' := ⋯, map_smul' := ⋯, map_one_eq_zero' := ⋯, leibniz' := ⋯ }

@[reducible]

noncomputable def CCDN.rationalDifferential (K : Type u_2) [Field K] : Differential (RatFunc K)

The differential field structure on RatFunc K given by formal rational differentiation; it is kept explicit to avoid introducing a competing global instance on rational functions.

Equations

• CCDN.rationalDifferential K = { deriv := Derivation.restrictScalars ℤ (CCDN.rationalDerivation K) }