prodCongrLeft_trans_prodComm — Mathlib

English

The composition of prodCongrLeft with prodComm equals the composition of prodComm with prodCongrRight: (prodCongrLeft e).trans (prodComm β₂ α₁) = (prodComm β₁ α₁).trans (prodCongrRight e).

Русский

Слияние prodCongrLeft с prodComm эквивалентно слиянию prodComm с prodCongrRight: (prodCongrLeft e).trans (prodComm β₂ α₁) = (prodComm β₁ α₁).trans (prodCongrRight e).

LaTeX

$$$(prodCongrLeft e).trans (prodComm \beta_2 \alpha_1) = (prodComm \beta_1 \alpha_1).trans (prodCongrRight e)$$$

Lean4

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

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