toIntLinearEquiv_trans — Mathlib

English

The Int-linearization functor commutes with transitive composition of additive equivalences: (e.trans e₂).toIntLinearEquiv = e.toIntLinearEquiv.trans e₂.toIntLinearEquiv.

Русский

Функтор Int-линейности сохраняет композицию эквивалентностей: (e.trans e₂).toIntLinearEquiv = e.toIntLinearEquiv.trans e₂.toIntLinearEquiv.

LaTeX

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

Lean4

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

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