Theorems · Definition · commutative algebra
IsDiscreteValuationRing.idealOrderIsoENat
(R : Type u_1) → [inst : CommRing R] → [inst_1 : IsDomain R] → [IsDiscreteValuationRing R] → Ideal R ≃o ℕ∞ᵒᵈ
The ideals of a discrete valuation ring are exactly the powers of the maximal ideal.
- Cited by
- 5 results in Mathlib
- Foundations
- Depth 97 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites15
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coeproof · cited by 62,936
- CommRingstatement and proof · cited by 17,173
- ENatstatement and proof · cited by 4,985
- Idealstatement and proof · cited by 4,748
- Bot.botproof · cited by 4,720
- IsDomainstatement and proof · cited by 2,196
- OrderDualstatement and proof · cited by 927
- OrderIsostatement · cited by 874
- OrderDual.toDualproof · cited by 481
- OrderDual.ofDualproof · cited by 400
- IsLocalRing.maximalIdealproof · cited by 297
- IsDiscreteValuationRingstatement and proof · cited by 117
Cited by5
Results whose statement or proof uses this declaration.
- IsDiscreteValuationRing.idealOrderIsoENat_symm_apply_coestatement · cited by 1
- IsDiscreteValuationRing.coheight_pow_maximalIdealproof · cited by 1
- IsDiscreteValuationRing.idealOrderIsoENat.congr_simpstatement and proof · cited by 0
- IsDiscreteValuationRing.idealOrderIsoENat_applystatement and proof · cited by 0
- IsDiscreteValuationRing.idealOrderIsoENat_symm_apply_coe_of_irreduciblestatement · cited by 0