prodCongr_symm — Mathlib

English

The product-congruence operation commutes with taking the symmetric (inverse) equivalences: (e₁.prodCongr e₂).symm = e₁.symm.prodCongr e₂.symm.

Русский

Операция произведения конгруэнций совместна с операцией взятия симметрии (обратной эквивалентности): (e₁.prodCongr e₂).symm = e₁.symm.prodCongr e₂.symm.

LaTeX

$$$ (e_1.prodCongr e_2)^{\mathrm{symm}} = e_1^{\mathrm{symm}}.prodCongr e_2^{\mathrm{symm}}. $$$

Lean4

@[simp]
theorem prodCongr_symm : (e₁.prodCongr e₂).symm = e₁.symm.prodCongr e₂.symm :=
  rfl

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