baseChangeHom — Mathlib

English

(r • f).baseChange A = r • (f.baseChange A).

Русский

(r • f).baseChange A = r • (f.baseChange A).

LaTeX

$$$$ (r\\cdot f).\\mathrm{baseChange}_A = r\\cdot (f.\\mathrm{baseChange}_A). $$$$

Lean4

/-- `baseChange` as a linear map.

When `M = N`, this is true more strongly as `Module.End.baseChangeHom`. -/
@[simps]
def baseChangeHom : (M →ₗ[R] N) →ₗ[R] A ⊗[R] M →ₗ[A] A ⊗[R] N
    where
  toFun := baseChange A
  map_add' := baseChange_add
  map_smul' := baseChange_smul

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