mk_coe — Mathlib

English

If f is a linear map A → M together with data h1 and h2 that certify the derivation axioms, then the derivation built from f has the same underlying function as f.

Русский

Если дана линейная карта f: A → M вместе с данными h1 и h2, подтверждающими выполнение аксиом вывода, то разновидность производной, построенная из f, имеет как функцию-основание ту же самую карту f.

LaTeX

$$$((f, h_1, h_2) : \mathrm{Derivation}(R,A,M))\!:\! A \to M = f.$$$

Lean4

@[simp]
theorem mk_coe (f : A →ₗ[R] M) (h₁ h₂) : ((⟨f, h₁, h₂⟩ : Derivation R A M) : A → M) = f :=
  rfl

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