mul'_tensor — Mathlib

English

For elements a ∈ A, b ∈ B, the action of mulLeft on a ⊗ b equals the tensor of mulLeft maps: mulLeft R (a ⊗ b) = map (mulLeft R a) (mulLeft R b).

Русский

Для элементов a ∈ A, b ∈ B выполнено: mulLeft на a ⊗ b равно тензору mulLeft(a) и mulLeft(b).

LaTeX

$$$\\mathrm{mulLeft}\\;R\\bigl(a\\otimes_R b\\bigr) = \\bigl(\\mathrm{map}(\\mathrm{mulLeft}\\;R\\;a) (\\mathrm{mulLeft}\\;R\\;b)\\bigr).$$$

Lean4

theorem mul'_tensor : mul' R (A ⊗[R] B) = map (mul' R A) (mul' R B) ∘ₗ tensorTensorTensorComm R A B A B :=
  ext_fourfold' <| by simp

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