Theorems · Definition · commutative algebra
UniqueFactorizationMonoid.factors
{α : Type u_1} → [inst : CommMonoidWithZero α] → [UniqueFactorizationMonoid α] → α → Multiset αNoncomputably determines the multiset of prime factors.
- Cited by
- 55 results in Mathlib
- Foundations
- Depth 19 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites4
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Multisetstatement · cited by 2,627
- CommMonoidWithZerostatement and proof · cited by 913
- UniqueFactorizationMonoidstatement and proof · cited by 279
- UniqueFactorizationMonoid.exists_prime_factorsproof · cited by 6
Cited by62
Results whose statement or proof uses this declaration.
- UniqueFactorizationMonoid.normalizedFactorsproof · cited by 151
- UniqueFactorizationMonoid.factors_prodstatement · cited by 18
- Associates.factors'proof · cited by 15
- UniqueFactorizationMonoid.irreducible_of_factorstatement and proof · cited by 13
- IsDedekindDomain.primesOverFinsetproof · cited by 11
- UniqueFactorizationMonoid.moebiusproof · cited by 10
- UniqueFactorizationMonoid.prime_of_factorstatement and proof · cited by 9
- UniqueFactorizationMonoid.factors_eq_normalizedFactorsstatement and proof · cited by 7
- UniqueFactorizationMonoid.dvd_of_mem_factorsstatement and proof · cited by 5
- IsAlgClosed.of_exists_rootproof · cited by 5
- Ideal.sum_ramification_inertiaproof · cited by 4
- UniqueFactorizationMonoid.exists_mem_factors_of_dvdstatement and proof · cited by 4