prodCongr_symm — Mathlib

English

The symmetry of prodCongr with respect to taking symm holds: (e1.prodCongr e2).symm = e1.symm.prodCongr e2.symm.

Русский

Симметрия prodCongr по отношению к взятию симм сохраняется: (e1.prodCongr e2).symm = e1.symm.prodCongr e2.symm.

LaTeX

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

Lean4

theorem prodCongr_symm : (e₁.prodCongr e₂).symm = e₁.symm.prodCongr e₂.symm :=
  rfl

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