R : Type u
S : Type v
T : Type w
A : Type z
a✝ b : R
n : ℕ
inst✝ : CommRing R
p✝ q p : R[X]
a : R
✝ : Nontrivial R
⊢ p %ₘ (X - ↑C a) = ↑C (eval a p)
R : Type u
S : Type v
T : Type w
A : Type z
a✝ b : R
n : ℕ
inst✝ : CommRing R
p✝ q p : R[X]
a : R
⊢ p %ₘ (X - ↑C a) = ↑C (eval a p)
nontriviality R
R : Type u
S : Type v
T : Type w
A : Type z
a✝ b : R
n : ℕ
inst✝ : CommRing R
p✝ q p : R[X]
a : R
✝ : Nontrivial R
h : eval a (p %ₘ (X - ↑C a)) = eval a p
⊢ p %ₘ (X - ↑C a) = ↑C (eval a p)
R : Type u
S : Type v
T : Type w
A : Type z
a✝ b : R
n : ℕ
inst✝ : CommRing R
p✝ q p : R[X]
a : R
✝ : Nontrivial R
⊢ p %ₘ (X - ↑C a) = ↑C (eval a p)
have h : (p %ₘ (X - C a)).eval a = p.eval a := by
  rw [modByMonic_eq_sub_mul_div _ (monic_X_sub_C a), eval_sub, eval_mul, eval_sub, eval_X,
    eval_C, sub_self, MulZeroClass.zero_mul, sub_zero]
R : Type u
S : Type v
T : Type w
A : Type z
a✝ b : R
n : ℕ
inst✝ : CommRing R
p✝ q p : R[X]
a : R
✝ : Nontrivial R
h : eval a (p %ₘ (X - ↑C a)) = eval a p
this : degree (p %ₘ (X - ↑C a)) < 1
⊢ p %ₘ (X - ↑C a) = ↑C (eval a p)
R : Type u
S : Type v
T : Type w
A : Type z
a✝ b : R
n : ℕ
inst✝ : CommRing R
p✝ q p : R[X]
a : R
✝ : Nontrivial R
h : eval a (p %ₘ (X - ↑C a)) = eval a p
⊢ p %ₘ (X - ↑C a) = ↑C (eval a p)
have : degree (p %ₘ (X - C a)) < 1 :=
  degree_X_sub_C a ▸ degree_modByMonic_lt p (monic_X_sub_C a)
R : Type u
S : Type v
T : Type w
A : Type z
a✝ b : R
n : ℕ
inst✝ : CommRing R
p✝ q p : R[X]
a : R
✝ : Nontrivial R
h : coeff (p %ₘ (X - ↑C a)) 0 = eval a p
this✝ : degree (p %ₘ (X - ↑C a)) < 1
this : degree (p %ₘ (X - ↑C a)) ≤ 0
⊢ p %ₘ (X - ↑C a) = ↑C (eval a p)
R : Type u
S : Type v
T : Type w
A : Type z
a✝ b : R
n : ℕ
inst✝ : CommRing R
p✝ q p : R[X]
a : R
✝ : Nontrivial R
h : eval a (p %ₘ (X - ↑C a)) = eval a p
this✝ : degree (p %ₘ (X - ↑C a)) < 1
this : degree (p %ₘ (X - ↑C a)) ≤ 0
⊢ p %ₘ (X - ↑C a) = ↑C (eval a p)
rw [eq_C_of_degree_le_zero this, eval_C] at h
no goals
R : Type u
S : Type v
T : Type w
A : Type z
a✝ b : R
n : ℕ
inst✝ : CommRing R
p✝ q p : R[X]
a : R
✝ : Nontrivial R
h : coeff (p %ₘ (X - ↑C a)) 0 = eval a p
this✝ : degree (p %ₘ (X - ↑C a)) < 1
this : degree (p %ₘ (X - ↑C a)) ≤ 0
⊢ p %ₘ (X - ↑C a) = ↑C (eval a p)
rw [eq_C_of_degree_le_zero this, h]
no goals
R : Type u
S : Type v
T : Type w
A : Type z
a✝ b : R
n : ℕ
inst✝ : CommRing R
p✝ q p : R[X]
a : R
✝ : Nontrivial R
⊢ eval a (p %ₘ (X - ↑C a)) = eval a p
rw [modByMonic_eq_sub_mul_div _ (monic_X_sub_C a), eval_sub, eval_mul, eval_sub, eval_X,
  eval_C, sub_self, MulZeroClass.zero_mul, sub_zero]
R : Type u
S : Type v
T : Type w
A : Type z
a✝ b : R
n : ℕ
inst✝ : CommRing R
p✝ q p : R[X]
a : R
✝ : Nontrivial R
h : eval a (p %ₘ (X - ↑C a)) = eval a p
⊢ degree (p %ₘ (X - ↑C a)) < 1 → degree (p %ₘ (X - ↑C a)) ≤ 0
R : Type u
S : Type v
T : Type w
A : Type z
a✝ b : R
n : ℕ
inst✝ : CommRing R
p✝ q p : R[X]
a : R
✝ : Nontrivial R
h : eval a (p %ₘ (X - ↑C a)) = eval a p
this : degree (p %ₘ (X - ↑C a)) < 1
⊢ degree (p %ₘ (X - ↑C a)) ≤ 0
revert this
case none
R : Type u
S : Type v
T : Type w
A : Type z
a✝ b : R
n : ℕ
inst✝ : CommRing R
p✝ q p : R[X]
a : R
✝ : Nontrivial R
h : eval a (p %ₘ (X - ↑C a)) = eval a p
⊢ none < 1 → none ≤ 0

case some
R : Type u
S : Type v
T : Type w
A : Type z
a✝ b : R
n : ℕ
inst✝ : CommRing R
p✝ q p : R[X]
a : R
✝ : Nontrivial R
h : eval a (p %ₘ (X - ↑C a)) = eval a p
val✝ : ℕ
⊢ some val✝ < 1 → some val✝ ≤ 0
R : Type u
S : Type v
T : Type w
A : Type z
a✝ b : R
n : ℕ
inst✝ : CommRing R
p✝ q p : R[X]
a : R
✝ : Nontrivial R
h : eval a (p %ₘ (X - ↑C a)) = eval a p
⊢ degree (p %ₘ (X - ↑C a)) < 1 → degree (p %ₘ (X - ↑C a)) ≤ 0
cases degree (p %ₘ (X - C a))
no goals
case none
R : Type u
S : Type v
T : Type w
A : Type z
a✝ b : R
n : ℕ
inst✝ : CommRing R
p✝ q p : R[X]
a : R
✝ : Nontrivial R
h : eval a (p %ₘ (X - ↑C a)) = eval a p
⊢ none < 1 → none ≤ 0
exact fun _ => bot_le
no goals
case some
R : Type u
S : Type v
T : Type w
A : Type z
a✝ b : R
n : ℕ
inst✝ : CommRing R
p✝ q p : R[X]
a : R
✝ : Nontrivial R
h : eval a (p %ₘ (X - ↑C a)) = eval a p
val✝ : ℕ
⊢ some val✝ < 1 → some val✝ ≤ 0
exact fun h => WithBot.some_le_some.2 (Nat.le_of_lt_succ (WithBot.some_lt_some.1 h))