English
Composition of linear equivalences over ℤ corresponds to composition of their AddEquiv counterparts: (e : M ≃+ M₂) and (e₂ : M₂ ≃+ M₃) give (e.trans e₂).toIntLinearEquiv = e.toIntLinearEquiv.trans e₂.toIntLinearEquiv.
Русский
Композиция линейных эквивалентностей над ℤ соответствует композиции их аддитивных эквивалентностей: (e.trans e₂).toIntLinearEquiv = e.toIntLinearEquiv.trans e₂.toIntLinearEquiv.
LaTeX
$$$$ (e.trans e_2).toIntLinearEquiv = e.toIntLinearEquiv.trans e_2.toIntLinearEquiv $$$$
Lean4
/-- The `R`-linear equivalence between additive morphisms `A →+ B` and `ℕ`-linear morphisms `A →ₗ[ℕ] B`.
-/
@[simps]
def addMonoidHomLequivNat {A B : Type*} (R : Type*) [Semiring R] [AddCommMonoid A] [AddCommMonoid B] [Module R B] :
(A →+ B) ≃ₗ[R] A →ₗ[ℕ] B where
toFun := AddMonoidHom.toNatLinearMap
invFun := LinearMap.toAddMonoidHom
map_add' _ _ := rfl
map_smul' _ _ := rfl
