mkDerivationEquiv_symm_apply — Mathlib

English

The inverse of mkDerivationEquiv sends a derivation D to its value on X, i.e. (mkDerivationEquiv R).symm D = D(X).

Русский

Обратное эквивалентности mkDerivationEquiv отправляет деривацию D в её значение на X: (mkDerivationEquiv R).symm D = D(X).

LaTeX

$$$(\\mathrm{mkDerivationEquiv}_R)^{-1}(D) = D X,$$$

Lean4

@[simp]
theorem mkDerivationEquiv_symm_apply (D : Derivation R R[X] A) : (mkDerivationEquiv R).symm D = D X :=
  rfl

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