restrictScalars — Mathlib

English

For any ContinuousLinearMap f, the restriction of its negation equals the negation of its restriction: (−f).restrictScalars R = −(f.restrictScalars R).

Русский

Для любого отображения f, ограничение на отрицательное отображение равно отрицательному ограничению: (−f).restrictScalars R = −(f.restrictScalars R).

LaTeX

$$$$ ( -f )_{|R} = -( f_{|R} ). $$$$

Lean4

/-- If `A` is an `R`-algebra, then a continuous `A`-linear map can be interpreted as a continuous
`R`-linear map. We assume `LinearMap.CompatibleSMul M₁ M₂ R A` to match assumptions of
`LinearMap.map_smul_of_tower`. -/
def restrictScalars (f : M₁ →L[A] M₂) : M₁ →L[R] M₂ :=
  ⟨(f : M₁ →ₗ[A] M₂).restrictScalars R, f.continuous⟩

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