tensorDistribEquiv_toLinearMap — Mathlib

English

Applying base change to a simple tensor yields the product with the base elements.

Русский

Применяя базовое изменение к простому тензору, получаем произведение базовых элементов.

LaTeX

$$$$ B_2.baseChange\ A (a \otimes m_2) (a' \otimes m_2') = (B_2 m_2 m_2') \cdot (a a'). $$$$

Lean4

@[simp]
theorem tensorDistribEquiv_toLinearMap : (tensorDistribEquiv R (M₁ := M₁) (M₂ := M₂)).toLinearMap = tensorDistrib R R :=
  by
  ext B₁ B₂ : 3
  ext
  exact mul_comm _ _

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