lTensor_tmul — Mathlib

English

The heterobasic map with identity components equals the identity map on the tensor product.

Русский

Гетеробазовое отображение с тождественными компонентами равно тождественному отображению на тензорном произведении.

LaTeX

$$$\text{map id id} = \mathrm{id}$$$

Lean4

@[simp]
theorem lTensor_tmul (f : N →ₗ[R] Q) (m : M) (n : N) : lTensor A M f (m ⊗ₜ[R] n) = m ⊗ₜ f n :=
  rfl

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