coeAddHom — Mathlib

English

The inclusion map extends to an AddHom from ℕ+ to ℕ, i.e., it preserves addition.

Русский

Включение расширяется до AddHom из ℕ+ в ℕ, то есть сохраняет сложение.

LaTeX

$$$ \\forall m,n \\in \\mathbb{N}^+,\\; \\mathrm{coe}(m+n) = \\mathrm{coe}(m) + \\mathrm{coe}(n). $$$$

Lean4

/-- `coe` promoted to an `AddHom`, that is, a morphism which preserves addition. -/
@[simps]
def coeAddHom : AddHom ℕ+ ℕ where
  toFun := (↑)
  map_add' := add_coe

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