sigmaEquivProd_sigmaCongrRight — Mathlib

English

The inverse composition (sigmaEquivProd α₁ β₁)^{-1} ∘ (sigmaCongrRight e) equals (prodCongrRight e) ∘ (sigmaEquivProd α₁ β₂)^{-1}.

Русский

Обратная компоновка (sigmaEquivProd α₁ β₁)^{-1} ∘ (sigmaCongrRight e) равна (prodCongrRight e) ∘ (sigmaEquivProd α₁ β₂)^{-1}.

LaTeX

$$$ (sigmaEquivProd α_1 β_1)^{-1} \circ (sigmaCongrRight e) = (prodCongrRight e) \circ (sigmaEquivProd α_1 β_2)^{-1}$$$

Lean4

theorem sigmaEquivProd_sigmaCongrRight :
    (sigmaEquivProd α₁ β₁).symm.trans (sigmaCongrRight e) = (prodCongrRight e).trans (sigmaEquivProd α₁ β₂).symm :=
  by
  ext ⟨a, b⟩ : 1
  simp only [trans_apply, sigmaCongrRight_apply, prodCongrRight_apply]
  rfl

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