toLinearMap_congr — Mathlib

English

Let f: M ≃ₗ[R] P and g: N ≃ₗ[R] Q be linear isomorphisms. Then the linear map on the tensor product induced by their congruence, (congr f g): M ⊗ N → P ⊗ Q, is exactly the canonical tensor product map map f g.

Русский

Пусть f: M ≃ₗ[R] P и g: N ≃ₗ[R] Q — линейные эквивалентности. Тогда линейное отображение, индуцируемое их сопоставлением конгруэнтности (congr f g): M ⊗ N → P ⊗ Q, совпадает с каноническим отображением tensor: map f g.

LaTeX

$$$ (congr f g)\\!\\toLinearMap = map f g $$$

Lean4

@[simp]
theorem toLinearMap_congr (f : M ≃ₗ[R] P) (g : N ≃ₗ[R] Q) : (congr f g).toLinearMap = map f g :=
  rfl

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