exists_mem_normalizedFactors — Mathlib

English

For x ≠ 0 and not a unit, there exists p with p ∈ normalizedFactors x.

Русский

Для x ≠ 0 и не единица существует p ∈ normalizedFactors x.

LaTeX

$$∃ p ∈ normalizedFactors(x)$$

Lean4

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

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