polynomialEquiv_comp_D — Mathlib

English

The polynomial equivalence intertwines the derivation with the differential: composing polynomialEquiv with D equals derivative'.

Русский

Эквивалентность полиномов соединяет производную и дифференциал: композиция polynomialEquiv и D равна derivative'.

LaTeX

$$$(polynomialEquiv \\; R) \\circ_\\mathrm{Der} (D \\; R \\; (Polynomial \\; R)) = \\mathrm{derivative'}$$$

Lean4

theorem polynomialEquiv_comp_D : (polynomialEquiv R).compDer (D R R[X]) = derivative' :=
  Derivation.liftKaehlerDifferential_comp _

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