val_mulMap_tmul — Mathlib

English

For a ∈ A and b ∈ B, the image of a ⊗ b under the disjointness-induced isomorphism equals the product a·b in S.

Русский

Пусть a ∈ A и b ∈ B. Образ a ⊗ b под изоморфизмом, соответствующим линейной несовместности, равен произведению a·b в S.

LaTeX

$$$\\ (A.mulMap)(a \\otimes_R b) = a \\cdot b$$$

Lean4

@[simp]
theorem val_mulMap_tmul (a : A) (b : B) : (H.mulMap (a ⊗ₜ[R] b) : S) = a.1 * b.1 :=
  rfl

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