symm_trans — Mathlib

English

The inverse of a transposed equivalence equals the transposed of the inverse composition.

Русский

Обратное к транспонированному эквиваленту равно транспонированному от обратной композиции.

LaTeX

$$$ (e_1.trans e_2)^{symm} = e_2^{symm}.trans e_1^{symm} $$$

Lean4

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

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