ext_nat — Mathlib

English

Let A be an additive monoid with zero. If f, g: ℕ →+ A satisfy f(1) = g(1), then f = g. Thus additive monoid homomorphisms from ℕ are determined by the image of 1.

Русский

Пусть A — аддитивный моноид с нулём. Если f, g: ℕ →+ A удовлетворяют f(1) = g(1), то f = g. Следовательно, аддитивные моноид-гомоморфизмы из ℕ полностью задаются образом единицы.

LaTeX

$$$ \forall A [AddZeroClass A], \forall f,g : \mathbb{N} \to_+ A, f(1) = g(1) \Rightarrow f = g $$$

Lean4

@[ext]
theorem ext_nat [AddZeroClass A] {f g : ℕ →+ A} : f 1 = g 1 → f = g :=
  ext_nat' f g

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