congr_tmul — Mathlib

English

Let f: M ≃ₗ[R] P and g: N ≃ₗ[R] Q be linear isomorphisms. Then for all m ∈ M, n ∈ N, congr f g sends m ⊗ n to f(m) ⊗ g(n).

Русский

Пусть f: M ≃ₗ[R] P и g: N ≃ₗ[R] Q — линейные эквивалентности. Тогда для всех m ∈ M, n ∈ N сопоставление congr f g отправляет m ⊗ n в f(m) ⊗ g(n).

LaTeX

$$$ congr\\ f\\ g\\ (m\\otimes n) = f(m)\\otimes g(n) $$$

Lean4

@[simp]
theorem congr_tmul (f : M ≃ₗ[R] P) (g : N ≃ₗ[R] Q) (m : M) (n : N) : congr f g (m ⊗ₜ n) = f m ⊗ₜ g n :=
  rfl

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