extendScalarsOfSurjective_apply — Mathlib

English

For a linear equivalence f : M ≃ₗ[R] N, extendScalarsOfSurjective h f equals f with the same underlying map and S-linearity, i.e., it commutes with evaluation.

Русский

Для линейного эквивалента f : M ≃ₗ[R] N переход extendScalarsOfSurjective h f эквивалентен самому f по базовой функции; сохраняется оценка значений.

LaTeX

$$$\\mathrm{extendScalarsOfSurjective}\; h\\; f : M \\simeq_{R} N \\to M \\simeq_{S} N$ и\\; (\\mathrm{extendScalarsOfSurjective}\; h\\; f)(x) = f(x)$$$

Lean4

@[simp]
theorem extendScalarsOfSurjective_apply (l : M →ₗ[R] N) (x) : l.extendScalarsOfSurjective h x = l x :=
  rfl

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