R : Type u
S : Type v
T : Type w
a b : R
n : ℕ
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : R[X]
hp : Monic p
r : R
ha : natDegree (X + ↑C r) = 0
⊢ False
R : Type u
S : Type v
T : Type w
a b : R
n : ℕ
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : R[X]
hp : Monic p
r : R
⊢ Monic (Polynomial.comp p (X + ↑C r))
refine' hp.comp (monic_X_add_C _) fun ha => _
R : Type u
S : Type v
T : Type w
a b : R
n : ℕ
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : R[X]
hp : Monic p
r : R
ha : 1 = 0
⊢ False
R : Type u
S : Type v
T : Type w
a b : R
n : ℕ
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : R[X]
hp : Monic p
r : R
ha : natDegree (X + ↑C r) = 0
⊢ False
rw [natDegree_X_add_C] at ha
no goals
R : Type u
S : Type v
T : Type w
a b : R
n : ℕ
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : R[X]
hp : Monic p
r : R
ha : 1 = 0
⊢ False
exact one_ne_zero ha