Theorems · Theorem · commutative algebra

irreducible_iff_prime_of_existsUnique_irreducible_factors

∀ {α : Type u_1} [inst : CommMonoidWithZero α] [IsCancelMulZero α],
  (∀ (a : α), a ≠ 0 → ∃ f, (∀ b ∈ f, Irreducible b) ∧ Associated f.prod a) →
    (∀ (f g : Multiset α),
        (∀ x ∈ f, Irreducible x) → (∀ x ∈ g, Irreducible x) → Associated f.prod g.prod → Multiset.Rel Associated f g) →
      ∀ (p : α), Irreducible p ↔ Prime p

Defined in

Mathlib.RingTheory.UniqueFactorizationDomain.Basic

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommMonoidWithZeroIsCancelMulZero