toIntLinearEquiv — Mathlib

English

There is a canonical linear equivalence between additive group endomorphisms and ℤ-linear endomorphisms, given by mapping an AddMonoidHom to its integer-linear extension, and vice versa.

Русский

Существует каноническое линейное эквивалентное отображение между концевыми отображениями аддитивной группы и ℤ-линейными эндоморфизмами: конвертация через целочисленное линейное продолжение и обратно.

LaTeX

$$$$ (A \\\\to_+ B) \\\\cong_ℤ (A \\\\to_ℤ B) $$$$

Lean4

/-- An additive equivalence between commutative additive groups is a linear
equivalence between ℤ-modules -/
def toIntLinearEquiv : M ≃ₗ[ℤ] M₂ :=
  e.toLinearEquiv fun c a ↦ e.toAddMonoidHom.map_zsmul a c

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