multiplesAddHom — Mathlib

English

If M is AddCommMonoid, there is an additive equivalence between M and (ℕ →+ M) given by x ↦ (n ↦ n • x) with inverse f ↦ f(1).

Русский

Если M — AddCommMonoid, существует аддитивное эквивалентное отображение между M и (ℕ →+ M), задаваемое x ↦ (n ↦ n • x) с обратным f ↦ f(1).

LaTeX

$$$ M \simeq_+ (\mathbb{N} \to_+ M)$$$

Lean4

/-- If `M` is commutative, `multiplesHom` is an additive equivalence. -/
def multiplesAddHom : M ≃+ (ℕ →+ M) where
  __ := multiplesHom M
  map_add' a b := AddMonoidHom.ext fun n ↦ by simp [nsmul_add]

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