toNatLinearEquiv — Mathlib

English

An additive equivalence between abelian monoids yields a linear equivalence over the natural numbers.

Русский

Аддитивное эквивалентное отображение между абелевыми моноидами порождает линейное эквивалентное отображение над натуральными числами.

LaTeX

$$$ toNatLinearEquiv : M \simeq_{\mathbb{N}} M_2 $$$

Lean4

/-- An additive equivalence between commutative additive monoids is a linear equivalence between
ℕ-modules -/
def toNatLinearEquiv : M ≃ₗ[ℕ] M₂ :=
  e.toLinearEquiv fun c a ↦ by rw [map_nsmul]

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