trans_symm — Mathlib

English

The symmetric of a transitive composition equals the transitive composition of the symmetric maps in reverse order.

Русский

Симметрическая часть транспитивной композиции равна транспитивной композиций симметрических отображений в обратном порядке.

LaTeX

$$$\\bigl(e_{12} \\text{.trans} e_{23}\\bigr)^{-1} = e_{23}^{-1} \\text{.trans} e_{12}^{-1}$$$

Lean4

@[simp]
theorem trans_symm : (e₁₂.trans e₂₃ : M₁ ≃ₛₗ[σ₁₃] M₃).symm = e₂₃.symm.trans e₁₂.symm :=
  rfl

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