coe_trans — Mathlib

English

The symmetrized AddEquiv corresponding to a LinearEquiv commutes with taking the underlying Symm.

Русский

Симметрированное AddEquiv, соответствующее LinearEquiv, коммутирует со взятием симметрии.

LaTeX

$$$\\mathrm{coe\\_toAddEquiv\\_symm}: (e_{12}.symm : M_2 \\to M_1) = (e_{12} : M_1 \\to M_2)^{-1}$$$

Lean4

theorem coe_trans : (e₁₂.trans e₂₃ : M₁ →ₛₗ[σ₁₃] M₃) = (e₂₃ : M₂ →ₛₗ[σ₂₃] M₃).comp (e₁₂ : M₁ →ₛₗ[σ₁₂] M₂) :=
  rfl

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