tensorEqLocus_tmul — Mathlib

English

There is a canonical map M ⊗ eqLocus f g → eqLocus (lTensor f) (lTensor g), compatible with the two tensor structures.

Русский

Существует каноническое отображение M ⊗ eqLocus f g → eqLocus (lTensor f) (lTensor g), совместимое с двумя тензорными структурами.

LaTeX

$$$\text{tensorEqLocus} : M ⊗_R eqLocus f g →_l[S] eqLocus( lTensor_S M f, lTensor_S M g )$$$

Lean4

@[simp]
theorem tensorEqLocus_tmul (m : M) (x : LinearMap.eqLocus f g) :
    (tensorEqLocus S M f g (m ⊗ₜ[R] x) : M ⊗[R] N) = m ⊗ₜ[R] (x : N) :=
  rfl

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