coe_coe — Mathlib

English

The coercion from Weight to Linear is compatible with evaluation: evaluating the linear realization equals χ.

Русский

Сопоставление веса линейному отображению согласовано с оценкой: значение линейного отображения равно χ.

LaTeX

$$$\\mathrm{coe\\_toLinear}(χ) = χ \\quad\\text{as functions on }L.$$$

Lean4

@[simp]
theorem coe_coe : (↑(χ : L →ₗ[R] R) : L → R) = (χ : L → R) :=
  rfl

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