congr_symm_tmul — Mathlib

English

Let f: M ≃ₗ[R] P and g: N ≃ₗ[R] Q be linear isomorphisms, and p ∈ P, q ∈ Q. Then the inverse congruence (congr f g).symm sends p ⊗ q to f.symm p ⊗ g.symm q.

Русский

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

LaTeX

$$$ (congr\\ f\\ g)^{-1}(p\\otimes q) = f^{-1}(p) \\otimes g^{-1}(q) $$$

Lean4

@[simp]
theorem congr_symm_tmul (f : M ≃ₗ[R] P) (g : N ≃ₗ[R] Q) (p : P) (q : Q) :
    (congr f g).symm (p ⊗ₜ q) = f.symm p ⊗ₜ g.symm q :=
  rfl

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