prodCongr_symm — Mathlib

English

The inverse of a product-congruence equals the product-congruence of the inverses: (e.prodCongr e').symm = e'.symm.prodCongr e. symm

Русский

Обратное к произведению конгруэнции равно конгруэнции обратных отображений: (e.prodCongr e').symm = e.symm.prodCongr e'.symm.

LaTeX

$$$$ (e.prodCongr e').symm = e.symm.prodCongr e'.symm. $$$$

Lean4

theorem prodCongr_symm [Module R₁ M₂] [Module R₁ M₃] [Module R₁ M₄] (e : M₁ ≃L[R₁] M₂) (e' : M₃ ≃L[R₁] M₄) :
    (e.prodCongr e').symm = e.symm.prodCongr e'.symm :=
  rfl

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