Theorems · Theorem · commutative algebra

UniqueFactorizationMonoid.exists_prime_factors

∀ {α : Type u_1} [inst : CommMonoidWithZero α] [UniqueFactorizationMonoid α] (a : α),
  a ≠ 0 → ∃ f, (∀ b ∈ f, Prime b) ∧ Associated f.prod a

Defined in

Mathlib.RingTheory.UniqueFactorizationDomain.Defs

Cited by

6 results in Mathlib

Foundations

Depth 18 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommMonoidWithZeroUniqueFactorizationMonoid