Theorems · Theorem · commutative algebra
Irreducible.maximalIdeal_eq
∀ {R : Type u} [inst : CommRing R] [inst_1 : IsDomain R] [inst_2 : IsDiscreteValuationRing R] {ϖ : R},
Irreducible ϖ → IsLocalRing.maximalIdeal R = Ideal.span {ϖ}- Cited by
- 5 results in Mathlib
- Foundations
- Depth 36 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites9
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Setstatement · cited by 53,352
- CommRingstatement and proof · cited by 17,173
- Idealstatement · cited by 4,748
- IsDomainstatement and proof · cited by 2,196
- Ideal.spanstatement · cited by 948
- Irreduciblestatement and proof · cited by 496
- IsLocalRing.maximalIdealstatement · cited by 297
- IsDiscreteValuationRingstatement and proof · cited by 117
- IsDiscreteValuationRing.irreducible_iff_uniformizerproof · cited by 4
Cited by5
Results whose statement or proof uses this declaration.
- IsDiscreteValuationRing.intValuation_maximalIdealproof · cited by 3
- Valuation.Integers.maximalIdeal_eq_setOfPred_le_v_algebraMapproof · cited by 2
- Valuation.Integers.maximalIdeal_pow_eq_setOfPred_le_v_algebraMap_powproof · cited by 2
- Valued.integer.totallyBounded_iff_finite_residueFieldproof · cited by 1
- IsDiscreteValuationRing.idealOrderIsoENat_symm_apply_coe_of_irreducibleproof · cited by 0