val_mulMap_tmul — Mathlib

English

If H is a linear disjointness isomorphism M ⊗ N ≃ M N, then it sends the pure tensor m ⊗ n to the product m · n in S.

Русский

Пусть существует изоморфизм H между M ⊗ N и MN; он отображает простое тензорное произведение m ⊗ n в произведение m n в S.

LaTeX

$$$(H.mulMap (m \otimes n) : S) = m.1 \cdot n.1$$$

Lean4

@[simp]
theorem val_mulMap_tmul (H : M.LinearDisjoint N) (m : M) (n : N) : (H.mulMap (m ⊗ₜ[R] n) : S) = m.1 * n.1 :=
  rfl

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