equivFinsuppOfBasisRight_apply_tmul

English

For a fixed i, (TensorProduct.equivFinsuppOfBasisRight 𝒞) (m ⊗ n) i equals 𝒞.repr n i · m.

Русский

Для фиксированного i выражение равно 𝒞.repr(n)i · m.

LaTeX

$$$ (TensorProduct.equivFinsuppOfBasisRight 𝒞) (m \otimes n) i = 𝒞.repr(n)(i) \cdot m $$$

Lean4

@[simp]
theorem equivFinsuppOfBasisRight_apply_tmul (m : M) (n : N) :
    (TensorProduct.equivFinsuppOfBasisRight 𝒞) (m ⊗ₜ n) = (𝒞.repr n).mapRange (· • m) (zero_smul _ _) := by ext;
  simp [equivFinsuppOfBasisRight]

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