linearCombination_one_tmul — Mathlib

English

For a fixed index set ι, the linear combination built from ones corresponds to a left tensor combination with finsuppScalarRight acting on the index set.

Русский

Для множества индексов ι линейная комбинация, построенная из единиц, эквивалентна левому тензорному сочетанию с finsuppScalarRight.

LaTeX

$$$ (linearCombination S ((1 : S) \\otimes_R v)).restrictScalars R = (linearCombination R v) \\circ (finsuppScalarRight R S ι)^{-1} $$$

Lean4

theorem linearCombination_one_tmul [DecidableEq ι] {v : ι → M} :
    (linearCombination S ((1 : S) ⊗ₜ[R] v ·)).restrictScalars R =
      (linearCombination R v).lTensor S ∘ₗ (finsuppScalarRight R S ι).symm :=
  by ext; simp [smul_tmul']

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