R : Type u
S : Type v
K : Type w
inst✝¹ : CommRing R
f : R[X]
inst✝ : IsDomain R
hf : degree f ≠ 0
⊢ ∀ (a : R), ↑(of f) a = 0 → a = 0
R : Type u
S : Type v
K : Type w
inst✝¹ : CommRing R
f : R[X]
inst✝ : IsDomain R
hf : degree f ≠ 0
⊢ Function.Injective ↑(of f)
rw [injective_iff_map_eq_zero]
R : Type u
S : Type v
K : Type w
inst✝¹ : CommRing R
f : R[X]
inst✝ : IsDomain R
hf : degree f ≠ 0
p : R
hp : ↑(of f) p = 0
⊢ p = 0
R : Type u
S : Type v
K : Type w
inst✝¹ : CommRing R
f : R[X]
inst✝ : IsDomain R
hf : degree f ≠ 0
⊢ ∀ (a : R), ↑(of f) a = 0 → a = 0
intro p hp
R : Type u
S : Type v
K : Type w
inst✝¹ : CommRing R
f : R[X]
inst✝ : IsDomain R
hf : degree f ≠ 0
p : R
hp : f ∣ ↑C p
⊢ p = 0
R : Type u
S : Type v
K : Type w
inst✝¹ : CommRing R
f : R[X]
inst✝ : IsDomain R
hf : degree f ≠ 0
p : R
hp : ↑(of f) p = 0
⊢ p = 0
rw [AdjoinRoot.of, RingHom.comp_apply, AdjoinRoot.mk_eq_zero] at hp
case pos
R : Type u
S : Type v
K : Type w
inst✝¹ : CommRing R
f : R[X]
inst✝ : IsDomain R
hf : degree f ≠ 0
p : R
hp : f ∣ ↑C p
h : f = 0
⊢ p = 0

case neg
R : Type u
S : Type v
K : Type w
inst✝¹ : CommRing R
f : R[X]
inst✝ : IsDomain R
hf : degree f ≠ 0
p : R
hp : f ∣ ↑C p
h : ¬f = 0
⊢ p = 0
R : Type u
S : Type v
K : Type w
inst✝¹ : CommRing R
f : R[X]
inst✝ : IsDomain R
hf : degree f ≠ 0
p : R
hp : f ∣ ↑C p
⊢ p = 0
by_cases h : f = 0
no goals
case pos
R : Type u
S : Type v
K : Type w
inst✝¹ : CommRing R
f : R[X]
inst✝ : IsDomain R
hf : degree f ≠ 0
p : R
hp : f ∣ ↑C p
h : f = 0
⊢ p = 0
exact C_eq_zero.mp (eq_zero_of_zero_dvd (by rwa [h] at hp))
no goals
R : Type u
S : Type v
K : Type w
inst✝¹ : CommRing R
f : R[X]
inst✝ : IsDomain R
hf : degree f ≠ 0
p : R
hp : f ∣ ↑C p
h : f = 0
⊢ 0 ∣ ↑C p
rwa [h] at hp
case neg
R : Type u
S : Type v
K : Type w
inst✝¹ : CommRing R
f : R[X]
inst✝ : IsDomain R
p : R
hp : f ∣ ↑C p
h : ¬f = 0
h_contra : p ≠ 0
⊢ degree f = 0
case neg
R : Type u
S : Type v
K : Type w
inst✝¹ : CommRing R
f : R[X]
inst✝ : IsDomain R
hf : degree f ≠ 0
p : R
hp : f ∣ ↑C p
h : ¬f = 0
⊢ p = 0
contrapose! hf with h_contra
case neg
R : Type u
S : Type v
K : Type w
inst✝¹ : CommRing R
f : R[X]
inst✝ : IsDomain R
p : R
hp : f ∣ ↑C p
h : ¬f = 0
h_contra : p ≠ 0
⊢ degree f = degree (↑C p)
case neg
R : Type u
S : Type v
K : Type w
inst✝¹ : CommRing R
f : R[X]
inst✝ : IsDomain R
p : R
hp : f ∣ ↑C p
h : ¬f = 0
h_contra : p ≠ 0
⊢ degree f = 0
rw [← degree_C h_contra]
R : Type u
S : Type v
K : Type w
inst✝¹ : CommRing R
f : R[X]
inst✝ : IsDomain R
p : R
hp : f ∣ ↑C p
h : ¬f = 0
h_contra : p ≠ 0
⊢ degree (↑C p) ≤ degree f
case neg
R : Type u
S : Type v
K : Type w
inst✝¹ : CommRing R
f : R[X]
inst✝ : IsDomain R
p : R
hp : f ∣ ↑C p
h : ¬f = 0
h_contra : p ≠ 0
⊢ degree f = degree (↑C p)
apply le_antisymm (degree_le_of_dvd hp (by rwa [Ne.def, C_eq_zero])) _
no goals
R : Type u
S : Type v
K : Type w
inst✝¹ : CommRing R
f : R[X]
inst✝ : IsDomain R
p : R
hp : f ∣ ↑C p
h : ¬f = 0
h_contra : p ≠ 0
⊢ degree (↑C p) ≤ degree f
rwa [degree_C h_contra, zero_le_degree_iff]
no goals
R : Type u
S : Type v
K : Type w
inst✝¹ : CommRing R
f : R[X]
inst✝ : IsDomain R
p : R
hp : f ∣ ↑C p
h : ¬f = 0
h_contra : p ≠ 0
⊢ ↑C p ≠ 0
rwa [Ne.def, C_eq_zero]