restrictScalars_apply — Mathlib

English

The value of the restricted map on an element x is the same as applying the original map to x; the underlying function does not change.

Русский

Значение ограниченного отображения на элементе x такое же, как и у исходного отображения; функция не изменяется.

LaTeX

$$$\\big( f\\text{ restricted}\\big)(x)=f(x)$$$

Lean4

@[simp]
theorem restrictScalars_apply (f : A →ₙₐ[S] B) (x : A) : f.restrictScalars R x = f x :=
  rfl

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