English
The symmetry of a product congruence equals the product congruence of symmetrics: (prodCongr e1 e2).symm = e1.symm.prodCongr e2.symm.
Русский
Симметрия конгруэнции произведения совпадает с конгруэнцией симметрических составляющих: (prodCongr e1 e2).symm = e1.symm.prodCongr e2.symm.
LaTeX
$$$(prodCongr e_1 e_2).symm = prodCongr e_1.symm e_2.symm$$$
Lean4
/-- Product of two equivalences. If `α₁ ≃ α₂` and `β₁ ≃ β₂`, then `α₁ × β₁ ≃ α₂ × β₂`. This is
`Prod.map` as an equivalence. -/
@[simps (attr := grind =) -fullyApplied apply]
def prodCongr {α₁ α₂ β₁ β₂} (e₁ : α₁ ≃ α₂) (e₂ : β₁ ≃ β₂) : α₁ × β₁ ≃ α₂ × β₂ :=
⟨Prod.map e₁ e₂, Prod.map e₁.symm e₂.symm, fun ⟨a, b⟩ => by simp, fun ⟨a, b⟩ => by simp⟩
