mulRightMap_eq_mulMap_comp — Mathlib

English

For any index type ι and m: ι → M, the left-map is equal to mulMap composed with rTensor and finsupp scalars.

Русский

Для любого индекса ι и семейства m: ι → M, левое отображение равно mulMap, композиции rTensor и finsupp-скалярирования.

LaTeX

$$mulLeftMap N m = mulMap M N ∘ₗ LinearMap.rTensor N (Finsupp.linearCombination R m) ∘ₗ (TensorProduct.finsuppScalarLeft R N ι).symm.toLinearMap$$

Lean4

theorem mulRightMap_eq_mulMap_comp {ι : Type*} [DecidableEq ι] (n : ι → N) :
    mulRightMap M n =
      mulMap M N ∘ₗ
        LinearMap.lTensor M (Finsupp.linearCombination R n) ∘ₗ
          (TensorProduct.finsuppScalarRight R M ι).symm.toLinearMap :=
  by ext; simp

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