R : Type u
S : Type ?u.257711
σ : Type v
M : Type w
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : AddCommGroup M
inst✝ : Module R M
r : R
hr : Prime r
⊢ Prime (↑C r)
R : Type u
S : Type ?u.257711
σ : Type v
M : Type w
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : AddCommGroup M
inst✝ : Module R M
r : R
⊢ Prime r → Prime (↑C r)
intro hr
R : Type u
S : Type ?u.257711
σ : Type v
M : Type w
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : AddCommGroup M
inst✝ : Module R M
r : R
hr : Prime r
this : r ≠ 0
⊢ Prime (↑C r)
R : Type u
S : Type ?u.257711
σ : Type v
M : Type w
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : AddCommGroup M
inst✝ : Module R M
r : R
hr : Prime r
⊢ Prime (↑C r)
have := hr.1
R : Type u
S : Type ?u.257711
σ : Type v
M : Type w
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : AddCommGroup M
inst✝ : Module R M
r : R
hr : Ideal.IsPrime (Ideal.span {r})
this : r ≠ 0
⊢ Ideal.IsPrime (Ideal.span {↑C r})

R : Type u
S : Type ?u.257711
σ : Type v
M : Type w
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : AddCommGroup M
inst✝ : Module R M
r : R
hr : Ideal.IsPrime (Ideal.span {r})
this : r ≠ 0
⊢ ↑C r ≠ 0

R : Type u
S : Type ?u.257711
σ : Type v
M : Type w
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : AddCommGroup M
inst✝ : Module R M
r : R
hr : Prime r
this : r ≠ 0
⊢ r ≠ 0
R : Type u
S : Type ?u.257711
σ : Type v
M : Type w
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : AddCommGroup M
inst✝ : Module R M
r : R
hr : Prime r
this : r ≠ 0
⊢ Prime (↑C r)
rw [← Ideal.span_singleton_prime] at hr⊢
R : Type u
S : Type ?u.257711
σ : Type v
M : Type w
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : AddCommGroup M
inst✝ : Module R M
r : R
hr : Ideal.IsPrime (Ideal.span {r})
this : r ≠ 0
⊢ Ideal.IsPrime (Ideal.map C (Ideal.span {r}))
R : Type u
S : Type ?u.257711
σ : Type v
M : Type w
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : AddCommGroup M
inst✝ : Module R M
r : R
hr : Ideal.IsPrime (Ideal.span {r})
this : r ≠ 0
⊢ Ideal.IsPrime (Ideal.span {↑C r})
rw [← Set.image_singleton, ← Ideal.map_span]
no goals
R : Type u
S : Type ?u.257711
σ : Type v
M : Type w
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : AddCommGroup M
inst✝ : Module R M
r : R
hr : Ideal.IsPrime (Ideal.span {r})
this : r ≠ 0
⊢ Ideal.IsPrime (Ideal.map C (Ideal.span {r}))
apply Ideal.isPrime_map_C_of_isPrime hr
R : Type u
S : Type ?u.257711
σ : Type v
M : Type w
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : AddCommGroup M
inst✝ : Module R M
r : R
hr : Ideal.IsPrime (Ideal.span {r})
this : r ≠ 0
h : ↑C r = 0
⊢ False
R : Type u
S : Type ?u.257711
σ : Type v
M : Type w
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : AddCommGroup M
inst✝ : Module R M
r : R
hr : Ideal.IsPrime (Ideal.span {r})
this : r ≠ 0
⊢ ↑C r ≠ 0
intro h
no goals
R : Type u
S : Type ?u.257711
σ : Type v
M : Type w
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : AddCommGroup M
inst✝ : Module R M
r : R
hr : Ideal.IsPrime (Ideal.span {r})
this : r ≠ 0
h : ↑C r = 0
⊢ False
apply (this (C_eq_zero.mp h))
no goals
R : Type u
S : Type ?u.257711
σ : Type v
M : Type w
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : AddCommGroup M
inst✝ : Module R M
r : R
hr : Prime r
this : r ≠ 0
⊢ r ≠ 0
assumption