R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DiscreteValuationRing R
⊢ ∃ ϖ, maximalIdeal R = span {ϖ}
R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DiscreteValuationRing R
⊢ ∃ ϖ, Irreducible ϖ
simp_rw [irreducible_iff_uniformizer]
no goals
R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DiscreteValuationRing R
⊢ ∃ ϖ, maximalIdeal R = span {ϖ}
exact (IsPrincipalIdealRing.principal <| maximalIdeal R).principal