coeFn_coe — Mathlib

English

For any LieDerivation f, the evaluation map equals its underlying linear map evaluation; i.e., applying the function part of f is the same as applying its linear map component.

Русский

Для любого LieDerivation f отображение применения функции совпадает с применением его линейного отображения; то есть функция f и линейное отображение совпадают по действию.

LaTeX

$$$\forall f:\, \text{LieDerivation } R\, L\, M,\; (f : L \to M) = f$$$

Lean4

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

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