eq_of_factorization_pos — Mathlib

English

If p is prime and q occurs in the prime factorization of p, then q = p.

Русский

Если p — простое и q встречается в факторизации p, то q = p.

LaTeX

$$$ \text{Prime}(p) \land p.factorization(q) \neq 0 \Rightarrow p = q $$$

Lean4

/-- The only prime factor of prime `p` is `p` itself. -/
theorem eq_of_factorization_pos {p q : ℕ} (hp : Prime p) (h : p.factorization q ≠ 0) : p = q := by
  simpa [hp.factorization, single_apply] using h

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