English
There is a canonical AddEquiv between additive morphisms A → B and ℤ-linear morphisms A →ₗ[ℤ] B, respecting the ℤ-structure.
Русский
Существует каноническое AddEquiv между аддитивными отображениями A → B и ℤ-линейными отображениями A →ₗ[ℤ] B, сохраняющее ℤ-структуру.
LaTeX
$$$$ (A \to_+ B) \\\\simeq_ℤ (A \\\\to_{ℤ} B) $$$$
Lean4
/-- The `R`-linear equivalence between additive morphisms `A →+ B` and `ℤ`-linear morphisms `A →ₗ[ℤ] B`.
-/
@[simps]
def addMonoidHomLequivInt {A B : Type*} (R : Type*) [Semiring R] [AddCommGroup A] [AddCommGroup B] [Module R B] :
(A →+ B) ≃ₗ[R] A →ₗ[ℤ] B where
toFun := AddMonoidHom.toIntLinearMap
invFun := LinearMap.toAddMonoidHom
map_add' _ _ := rfl
map_smul' _ _ := rfl
