exists_mem_factors — Mathlib

English

If x ≠ 0 and x is not a unit, then x has a prime factor in its factorization.

Русский

Если x ≠ 0 и не является единицей, то в разложении x есть простый фактор.

LaTeX

$$$x \neq 0 \;\Rightarrow\; x \text{ не единица} \Rightarrow \exists p \in \mathrm{factors}(x).$$$

Lean4

theorem exists_mem_factors {x : α} (hx : x ≠ 0) (h : ¬IsUnit x) : ∃ p, p ∈ factors x :=
  by
  obtain ⟨p', hp', hp'x⟩ := WfDvdMonoid.exists_irreducible_factor h hx
  obtain ⟨p, hp, _⟩ := exists_mem_factors_of_dvd hx hp' hp'x
  exact ⟨p, hp⟩

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