toNatLinearEquiv_trans — Mathlib

English

For e : M ≃+ M₂ and e₂ : M₂ ≃+ M₃, the Nat-linearization respects trans: (e.trans e₂).toNatLinearEquiv = e.toNatLinearEquiv.trans e₂.toNatLinearEquiv.

Русский

Для e : M ≃+ M₂ и e₂ : M₂ ≃+ M₃ тождество сохранения транзитивности: (e.trans e₂).toNatLinearEquiv = e.toNatLinearEquiv.trans e₂.toNatLinearEquiv.

LaTeX

$$$$ (e.trans e_2).toNatLinearEquiv = e.toNatLinearEquiv.trans e_2.toNatLinearEquiv $$$$

Lean4

@[simp]
theorem toNatLinearEquiv_trans (e₂ : M₂ ≃+ M₃) :
    (e.trans e₂).toNatLinearEquiv = e.toNatLinearEquiv.trans e₂.toNatLinearEquiv :=
  rfl

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