Theorems · Theorem · commutative algebra
IsDiscreteValuationRing.HasUnitMulPowIrreducibleFactorization.toUniqueFactorizationMonoid
∀ {R : Type u_1} [inst : CommRing R] [IsCancelMulZero R],
IsDiscreteValuationRing.HasUnitMulPowIrreducibleFactorization R → UniqueFactorizationMonoid RAn integral domain in which there is an irreducible element p
such that every nonzero element is associated to a power of p is a unique factorization domain.
See IsDiscreteValuationRing.ofHasUnitMulPowIrreducibleFactorization.
- Cited by
- 1 results in Mathlib
- Foundations
- Depth 36 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- CommRingIsCancelMulZero
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites24
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- CommRingstatement and proof · cited by 17,173
- one_mulproof · cited by 2,841
- Unitsproof · cited by 2,804
- Units.valproof · cited by 1,966
- mul_assocproof · cited by 1,667
- pow_zeroproof · cited by 1,094
- Irreducibleproof · cited by 496
- Associatedproof · cited by 296
- UniqueFactorizationMonoidstatement · cited by 279
- Primeproof · cited by 277
- pow_succ'proof · cited by 228
- mul_left_commproof · cited by 184
Cited by1
Results whose statement or proof uses this declaration.
- IsDiscreteValuationRing.ofHasUnitMulPowIrreducibleFactorizationproof · cited by 0