Theorems · Theorem · commutative algebra
UniqueFactorizationMonoid.of_exists_prime_factors
∀ {α : Type u_1} [inst : CommMonoidWithZero α] [IsCancelMulZero α],
(∀ (a : α), a ≠ 0 → ∃ f, (∀ b ∈ f, Prime b) ∧ Associated f.prod a) → UniqueFactorizationMonoid α- Cited by
- 4 results in Mathlib
- Foundations
- Depth 35 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites10
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Multisetstatement and proof · cited by 2,627
- CommMonoidWithZerostatement and proof · cited by 913
- Multiset.prodstatement and proof · cited by 528
- Associatedstatement and proof · cited by 296
- UniqueFactorizationMonoidstatement · cited by 279
- Primestatement and proof · cited by 277
- IsCancelMulZerostatement and proof · cited by 177
- WfDvdMonoidproof · cited by 37
- irreducible_iff_prime_of_exists_prime_factorsproof · cited by 1
- WfDvdMonoid.of_exists_prime_factorsproof · cited by 1
Cited by4
Results whose statement or proof uses this declaration.
- UniqueFactorizationMonoid.iff_exists_prime_factorsproof · cited by 1
- Submonoid.LocalizationMap.uniqueFactorizationMonoidproof · cited by 1
- UniqueFactorizationMonoid.of_existsUnique_irreducible_factorsproof · cited by 0