Theorems · Theorem · commutative algebra
IsDiscreteValuationRing.eq_unit_mul_pow_irreducible
∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDomain R] [IsDiscreteValuationRing R] {x : R},
x ≠ 0 → ∀ {ϖ : R}, Irreducible ϖ → ∃ n u, x = ↑u * ϖ ^ n- Cited by
- 6 results in Mathlib
- Foundations
- Depth 93 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.
- CommRingstatement and proof · cited by 17,173
- Unitsstatement and proof · cited by 2,804
- mul_commproof · cited by 2,262
- IsDomainstatement and proof · cited by 2,196
- Units.valstatement and proof · cited by 1,966
- Irreduciblestatement and proof · cited by 496
- Associatedproof · cited by 296
- IsDiscreteValuationRingstatement and proof · cited by 117
- Associated.symmproof · cited by 87
- IsDiscreteValuationRing.associated_pow_irreducibleproof · cited by 4
Cited by6
Results whose statement or proof uses this declaration.
- Ring.ord_eq_addValproof · cited by 3
- IsDiscreteValuationRing.intValuation_maximalIdealproof · cited by 3
- IsDiscreteValuationRing.exists_lift_of_le_oneproof · cited by 2
- IsDiscreteValuationRing.addVal_eq_zero_iffproof · cited by 0
- IsDiscreteValuationRing.exists_units_eq_smul_zpow_of_irreducibleproof · cited by 0
- IsDiscreteValuationRing.addVal_eq_iff_associatedproof · cited by 0