apply — Mathlib

English

The canonical coe to LinearMap agrees with the underlying function of a semilinear isometry.

Русский

Каноническое приведение к LinearMap совпадает с базовой функцией семилинейной изометрии.

LaTeX

$$$\forall f,\ \text{toLinearMap}(f) = f$$$

Lean4

/-- See Note [custom simps projection]. We need to specify this projection explicitly in this case,
  because it is a composition of multiple projections. -/
def apply (σ₁₂ : R →+* R₂) (E E₂ : Type*) [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E]
    [Module R₂ E₂] (h : E →ₛₗᵢ[σ₁₂] E₂) : E → E₂ :=
  h

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