prodCongr_symm_apply — Mathlib

English

The inverse of prodCongr acts by the standard product-congruence inverse: (prodCongr l r).symm x = (Equiv.prodCongr l r).symm x.

Русский

Обратное к prodCongr действует через стандартную обратную конгруэнцию произведения: (prodCongr l r).symm x = (Equiv.prodCongr l r).symm x.

LaTeX

$$$$ (prodCongr l r).symm x = (Equiv.prodCongr l r).symm x. $$$$

Lean4

@[simp low]
theorem prodCongr_symm_apply (x : A × B) : (prodCongr l r).symm x = (Equiv.prodCongr l r).symm x :=
  rfl

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