extendScalarsOfSurjective — Mathlib

English

For any l : M →ₗ[R] N, applying extendScalarsOfSurjective to l yields the same function: (l.extendScalarsOfSurjective h) x = l x.

Русский

Для любого отображения l: M →ₗ[R] N выполнение extendScalarsOfSurjective над l даёт ту же самую функцию: (l.extendScalarsOfSurjective h) x = l x.

LaTeX

$$$\\forall l:\\, M \\to_{R} N:\\; (l.extendScalarsOfSurjective\th)\,x = l\,x$$$

Lean4

/-- If `R →+* S` is surjective, then `R`-linear maps are also `S`-linear. -/
abbrev extendScalarsOfSurjective (h : Surjective (algebraMap R S)) (l : M →ₗ[R] N) : M →ₗ[S] N :=
  extendScalarsOfSurjectiveEquiv h l

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