coe_restrictScalars — Mathlib

English

Treat ContinuousLinearMap.restrictScalars as a linear map between appropriate modules, preserving addition and scalar actions.

Русский

Рассматривая ContinuousLinearMap.restrictScalars как линейное отображение между соответствующими модулями, сохраняются сложение и действия скалярных полей.

LaTeX

$$$$ (f + g)_{|R} = f_{|R} + g_{|R}, \quad (rf)_{|R} = r (f_{|R}). $$$$

Lean4

@[simp]
theorem coe_restrictScalars (f : M₁ →L[A] M₂) :
    (f.restrictScalars R : M₁ →ₗ[R] M₂) = (f : M₁ →ₗ[A] M₂).restrictScalars R :=
  rfl

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