R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
⊢ Ideal.span {X} = RingHom.ker (constantCoeff R)
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
⊢ Ideal.IsPrime (Ideal.span {X})
suffices Ideal.span ({X} : Set (PowerSeries R)) = RingHom.ker (constantCoeff R) by
  rw [this]
  exact RingHom.ker_isPrime _
case h
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
⊢ ∀ (x : PowerSeries R), x ∈ Ideal.span {X} ↔ x ∈ RingHom.ker (constantCoeff R)
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
⊢ Ideal.span {X} = RingHom.ker (constantCoeff R)
apply Ideal.ext
case h
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
φ : PowerSeries R
⊢ φ ∈ Ideal.span {X} ↔ φ ∈ RingHom.ker (constantCoeff R)
case h
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
⊢ ∀ (x : PowerSeries R), x ∈ Ideal.span {X} ↔ x ∈ RingHom.ker (constantCoeff R)
intro φ
no goals
case h
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
φ : PowerSeries R
⊢ φ ∈ Ideal.span {X} ↔ φ ∈ RingHom.ker (constantCoeff R)
rw [RingHom.mem_ker, Ideal.mem_span_singleton, X_dvd_iff]
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
this : Ideal.span {X} = RingHom.ker (constantCoeff R)
⊢ Ideal.IsPrime (RingHom.ker (constantCoeff R))
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
this : Ideal.span {X} = RingHom.ker (constantCoeff R)
⊢ Ideal.IsPrime (Ideal.span {X})
rw [this]
no goals
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
this : Ideal.span {X} = RingHom.ker (constantCoeff R)
⊢ Ideal.IsPrime (RingHom.ker (constantCoeff R))
exact RingHom.ker_isPrime _