prodCongrRight_trans_prodComm — Mathlib

English

The composition (prodCongrRight e).trans (prodComm α₁ β₂) equals (prodComm α₁ β₁).trans (prodCongrLeft e).

Русский

Композиция (prodCongrRight e).trans (prodComm α₁ β₂) равна (prodComm α₁ β₁).trans (prodCongrLeft e).

LaTeX

$$(prodCongrRight e).trans (prodComm α₁ β₂) = (prodComm α₁ β₁).trans (prodCongrLeft e)$$

Lean4

@[simp]
theorem prodCongrRight_trans_prodComm :
    (prodCongrRight e).trans (prodComm _ _) = (prodComm _ _).trans (prodCongrLeft e) :=
  by
  ext ⟨a, b⟩ : 1
  simp

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