coeFn_coe — Mathlib

English

The coercion from derivations to their underlying linear maps is injective: if two derivations have the same linear map, they are equal.

Русский

Коэрcия преобразования производной к линейному отображению инъективна: если две производные имеют одинаковое линейное отображение, то они равны.

LaTeX

$$Injectivity of the map D \mapsto (D : A → M).$$

Lean4

@[simp, norm_cast]
theorem coeFn_coe (f : Derivation R A M) : ⇑(f : A →ₗ[R] M) = f :=
  rfl

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