exists_prime_factors — Mathlib

English

In a CancelCommMonoidWithZero α that is a UniqueFactorizationMonoid, for any a ≠ 0 there exists a multiset f consisting only of primes such that f.prod is associated to a.

Русский

В последовательном моноиде α, являющемся уникальным факторизационным моноидом, для любого a ≠ 0 существует мультисет f, состоящий только из простых, такое что произведение f ассоциировано с a.

LaTeX

$$$\forall a\ (a \neq 0) \Rightarrow \exists f : \mathrm{Multiset}\ α,\ (\forall b \in f, \mathrm{Prime}(b)) \land f.prod ~ᵤ a.$$$

Lean4

theorem exists_prime_factors (a : α) : a ≠ 0 → ∃ f : Multiset α, (∀ b ∈ f, Prime b) ∧ f.prod ~ᵤ a :=
  by
  simp_rw [← UniqueFactorizationMonoid.irreducible_iff_prime]
  apply WfDvdMonoid.exists_factors a

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