baseChange_eq_ltensor — Mathlib

English

The base-change of a linear map f is the same as its left-tensor construction: baseChange_A(f) = f.lTensor_A, i.e., the same A-linear map A ⊗_R M →_A A ⊗_R N.

Русский

Расширение по основанию от линейного отображения f совпадает с его левой тензорной конструкцией: baseChange_A(f) = f.lTensor_A.

LaTeX

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

Lean4

theorem baseChange_eq_ltensor : (f.baseChange A : A ⊗ M → A ⊗ N) = f.lTensor A :=
  rfl

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