coe_symm_trans — Mathlib

English

The symmetry of the transpose corresponds to the composition of the symmetry of the components.

Русский

Симметрия транспонирования соответствует композиции симметрии компонентов.

LaTeX

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

Lean4

theorem coe_symm_trans (e₁ : E ≃ₛₗᵢ[σ₁₂] E₂) (e₂ : E₂ ≃ₛₗᵢ[σ₂₃] E₃) : ⇑(e₁.trans e₂).symm = e₁.symm ∘ e₂.symm :=
  rfl

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