prodCongr_symm — Mathlib

English

The inverse of the product congruence equals the product of the inverses: (e1.prodCongr e2)^{-1} = e1^{-1}.prodCongr e2^{-1}.

Русский

Обратное произведения конгруэнции равно произведению обратных: (e1.prodCongr e2)^{-1} = e1^{-1}.prodCongr e2^{-1}.

LaTeX

$$$(e_1 \!\cdot\! e_2)^{-1} = e_1^{-1} \cdot e_2^{-1}$$$

Lean4

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

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