factorization_inj — Mathlib

English

The map n ↦ n.factorization is injective on the set of positive naturals.

Русский

Отображение n ↦ n.factorization инъективно на множества положительных чисел.

LaTeX

$$$\text{Nat.factorization}: \{ n>0\} \to (\mathbb{N} \to\mathbb{N}) \text{ is injective}$$$

Lean4

/-- Every nonzero natural number has a unique prime factorization -/
theorem factorization_inj : Set.InjOn factorization {x : ℕ | x ≠ 0} := fun a ha b hb h =>
  eq_of_factorization_eq ha hb fun p => by simp [h]

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