Theorem: Prime.ideal_span_singleton_isPrime (FormalisingMathematics2024/Solutions/Section14UFDsAndPIDsEtc/Sheet3.lean)

State before:
R✝ : Type
inst✝³ : CommRing R✝
inst✝² : IsDomain R✝
inst✝¹ : UniqueFactorizationMonoid R✝
R : Type
inst✝ : CommRing R
p : R
hp : Prime p
⊢ Ideal.IsPrime (Ideal.span {p})
Tactic:
rwa [Ideal.span_singleton_prime]
State after:
R✝ : Type
inst✝³ : CommRing R✝
inst✝² : IsDomain R✝
inst✝¹ : UniqueFactorizationMonoid R✝
R : Type
inst✝ : CommRing R
p : R
hp : Prime p
⊢ p ≠ 0

State before:
R✝ : Type
inst✝³ : CommRing R✝
inst✝² : IsDomain R✝
inst✝¹ : UniqueFactorizationMonoid R✝
R : Type
inst✝ : CommRing R
p : R
hp : Prime p
⊢ p ≠ 0
Tactic:
exact hp.ne_zero
State after:
no goals