congr_mul — Mathlib

English

Symmetry for tmul under congr: (congr f g).symm (p ⊗ q) = f.symm p ⊗ g.symm q.

Русский

Симметрия для tmul под congr: (congr f g).symm (p ⊗ q) = f.symm p ⊗ g.symm q.

LaTeX

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

Lean4

theorem congr_mul (f₁ f₂ : M ≃ₗ[A] M) (g₁ g₂ : N ≃ₗ[R] N) : congr (f₁ * f₂) (g₁ * g₂) = congr f₁ g₁ * congr f₂ g₂ :=
  congr_trans _ _ _ _

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