coe_toAddEquiv_symm — Mathlib

English

Linear equivalences are closed under composition: the composition e1₂.trans e₂₃ is a linear equivalence from M1 to M3 with the expected action.

Русский

Линейные эквивалентности замыкаются по композиции: композиция e1₂.trans e2₃ образует линейную эквивалентность между M1 и M3.

LaTeX

$$$e_{12} \;\\text{trans} \\; e_{23} : M_1 \\to M_3 = e_{23} \\circ e_{12}$$$

Lean4

theorem coe_toAddEquiv_symm : (e₁₂.symm : M₂ ≃+ M₁) = (e₁₂ : M₁ ≃+ M₂).symm :=
  rfl

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