equivFinsuppOfBasisLeft_apply_tmul

English

Applying the left basis-equivariant map to m ⊗ n yields the left basis representation of m scaled by n.

Русский

Применение левого базисного эквивалента к m ⊗ n даёт представление m, масштабированное n.

LaTeX

$$(TensorProduct.equivFinsuppOfBasisLeft \mathcal{B}) (m ⊗ₜ n) i = \mathcal{B}.repr(m) i · n$$

Lean4

@[simp]
theorem equivFinsuppOfBasisLeft_apply_tmul (m : M) (n : N) :
    (TensorProduct.equivFinsuppOfBasisLeft ℬ) (m ⊗ₜ n) = (ℬ.repr m).mapRange (· • n) (zero_smul _ _) := by
  simp [equivFinsuppOfBasisLeft]

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