[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
A' : Type u_1
B' : Type u_2
a b : R
n : ℕ
inst✝⁴ : CommSemiring A'
inst✝³ : Semiring B'
inst✝² : CommSemiring R
p✝ q r✝ : R[X]
inst✝¹ : Semiring A
inst✝ : Algebra R A
r : R
p : (fun x => A[X]) r
⊢ (↑(RingHom.comp C (algebraMap R A)) r * p).toFinsupp = (p * ↑(RingHom.comp C (algebraMap R A)) r).toFinsupp
[PROOFSTEP]
dsimp only [RingHom.toFun_eq_coe, RingHom.comp_apply]
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
A' : Type u_1
B' : Type u_2
a b : R
n : ℕ
inst✝⁴ : CommSemiring A'
inst✝³ : Semiring B'
inst✝² : CommSemiring R
p✝ q r✝ : R[X]
inst✝¹ : Semiring A
inst✝ : Algebra R A
r : R
p : (fun x => A[X]) r
⊢ (↑C (↑(algebraMap R A) r) * p).toFinsupp = (p * ↑C (↑(algebraMap R A) r)).toFinsupp
[PROOFSTEP]
simp_rw [toFinsupp_mul, toFinsupp_C]
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
A' : Type u_1
B' : Type u_2
a b : R
n : ℕ
inst✝⁴ : CommSemiring A'
inst✝³ : Semiring B'
inst✝² : CommSemiring R
p✝ q r✝ : R[X]
inst✝¹ : Semiring A
inst✝ : Algebra R A
r : R
p : (fun x => A[X]) r
⊢ AddMonoidAlgebra.single 0 (↑(algebraMap R A) r) * p.toFinsupp =
    p.toFinsupp * AddMonoidAlgebra.single 0 (↑(algebraMap R A) r)
[PROOFSTEP]
convert Algebra.commutes' r p.toFinsupp
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
A' : Type u_1
B' : Type u_2
a b : R
n : ℕ
inst✝⁴ : CommSemiring A'
inst✝³ : Semiring B'
inst✝² : CommSemiring R
p✝ q r✝ : R[X]
inst✝¹ : Semiring A
inst✝ : Algebra R A
r : R
p : (fun x => A[X]) r
⊢ (r • p).toFinsupp = (↑(RingHom.comp C (algebraMap R A)) r * p).toFinsupp
[PROOFSTEP]
dsimp only [RingHom.toFun_eq_coe, RingHom.comp_apply]
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
A' : Type u_1
B' : Type u_2
a b : R
n : ℕ
inst✝⁴ : CommSemiring A'
inst✝³ : Semiring B'
inst✝² : CommSemiring R
p✝ q r✝ : R[X]
inst✝¹ : Semiring A
inst✝ : Algebra R A
r : R
p : (fun x => A[X]) r
⊢ (r • p).toFinsupp = (↑C (↑(algebraMap R A) r) * p).toFinsupp
[PROOFSTEP]
rw [toFinsupp_smul, toFinsupp_mul, toFinsupp_C]
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
A' : Type u_1
B' : Type u_2
a b : R
n : ℕ
inst✝⁴ : CommSemiring A'
inst✝³ : Semiring B'
inst✝² : CommSemiring R
p✝ q r✝ : R[X]
inst✝¹ : Semiring A
inst✝ : Algebra R A
r : R
p : (fun x => A[X]) r
⊢ r • p.toFinsupp = AddMonoidAlgebra.single 0 (↑(algebraMap R A) r) * p.toFinsupp
[PROOFSTEP]
exact Algebra.smul_def' _ _
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
A' : Type u_1
B' : Type u_2
a b : R
n : ℕ
inst✝⁴ : CommSemiring A'
inst✝³ : Semiring B'
inst✝² : CommSemiring R
p q r✝ : R[X]
inst✝¹ : Semiring A
inst✝ : Algebra R A
r : R
⊢ (↑C (↑(algebraMap R A) r)).toFinsupp = ↑(algebraMap R (AddMonoidAlgebra A ℕ)) r
[PROOFSTEP]
rw [toFinsupp_C]
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
A' : Type u_1
B' : Type u_2
a b : R
n : ℕ
inst✝⁴ : CommSemiring A'
inst✝³ : Semiring B'
inst✝² : CommSemiring R
p q r✝ : R[X]
inst✝¹ : Semiring A
inst✝ : Algebra R A
r : R
⊢ AddMonoidAlgebra.single 0 (↑(algebraMap R A) r) = ↑(algebraMap R (AddMonoidAlgebra A ℕ)) r
[PROOFSTEP]
rfl
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
A' : Type u_1
B' : Type u_2
a b : R
n : ℕ
inst✝⁴ : CommSemiring A'
inst✝³ : Semiring B'
inst✝² : CommSemiring R
p q r✝ : R[X]
inst✝¹ : Semiring A
inst✝ : Algebra R A
src✝ : R[X] ≃+* AddMonoidAlgebra R ℕ := toFinsuppIso R
r : R
⊢ Equiv.toFun src✝.toEquiv (↑(algebraMap R R[X]) r) = ↑(algebraMap R (AddMonoidAlgebra R ℕ)) r
[PROOFSTEP]
dsimp
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
A' : Type u_1
B' : Type u_2
a b : R
n : ℕ
inst✝⁴ : CommSemiring A'
inst✝³ : Semiring B'
inst✝² : CommSemiring R
p q r✝ : R[X]
inst✝¹ : Semiring A
inst✝ : Algebra R A
src✝ : R[X] ≃+* AddMonoidAlgebra R ℕ := toFinsuppIso R
r : R
⊢ (↑(algebraMap R R[X]) r).toFinsupp = AddMonoidAlgebra.single 0 r
[PROOFSTEP]
exact toFinsupp_algebraMap _
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
A' : Type u_1
B' : Type u_2
a b : R
n : ℕ
inst✝⁵ : CommSemiring A'
inst✝⁴ : Semiring B'
inst✝³ : CommSemiring R
p q r : R[X]
inst✝² : Semiring A
inst✝¹ : Algebra R A
inst✝ : Nontrivial A
⊢ ⊥ ≠ ⊤
[PROOFSTEP]
rw [Ne.def, SetLike.ext_iff, not_forall]
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
A' : Type u_1
B' : Type u_2
a b : R
n : ℕ
inst✝⁵ : CommSemiring A'
inst✝⁴ : Semiring B'
inst✝³ : CommSemiring R
p q r : R[X]
inst✝² : Semiring A
inst✝¹ : Algebra R A
inst✝ : Nontrivial A
⊢ ∃ x, ¬(x ∈ ⊥ ↔ x ∈ ⊤)
[PROOFSTEP]
refine' ⟨X, _⟩
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
A' : Type u_1
B' : Type u_2
a b : R
n : ℕ
inst✝⁵ : CommSemiring A'
inst✝⁴ : Semiring B'
inst✝³ : CommSemiring R
p q r : R[X]
inst✝² : Semiring A
inst✝¹ : Algebra R A
inst✝ : Nontrivial A
⊢ ¬(X ∈ ⊥ ↔ X ∈ ⊤)
[PROOFSTEP]
simp only [Algebra.mem_bot, not_exists, Set.mem_range, iff_true_iff, Algebra.mem_top, algebraMap_apply, not_forall]
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
A' : Type u_1
B' : Type u_2
a b : R
n : ℕ
inst✝⁵ : CommSemiring A'
inst✝⁴ : Semiring B'
inst✝³ : CommSemiring R
p q r : R[X]
inst✝² : Semiring A
inst✝¹ : Algebra R A
inst✝ : Nontrivial A
⊢ ∀ (x : R), ¬↑C (↑(algebraMap R A) x) = X
[PROOFSTEP]
intro x
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
A' : Type u_1
B' : Type u_2
a b : R
n : ℕ
inst✝⁵ : CommSemiring A'
inst✝⁴ : Semiring B'
inst✝³ : CommSemiring R
p q r : R[X]
inst✝² : Semiring A
inst✝¹ : Algebra R A
inst✝ : Nontrivial A
x : R
⊢ ¬↑C (↑(algebraMap R A) x) = X
[PROOFSTEP]
rw [ext_iff, not_forall]
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
A' : Type u_1
B' : Type u_2
a b : R
n : ℕ
inst✝⁵ : CommSemiring A'
inst✝⁴ : Semiring B'
inst✝³ : CommSemiring R
p q r : R[X]
inst✝² : Semiring A
inst✝¹ : Algebra R A
inst✝ : Nontrivial A
x : R
⊢ ∃ x_1, ¬coeff (↑C (↑(algebraMap R A) x)) x_1 = coeff X x_1
[PROOFSTEP]
refine' ⟨1, _⟩
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
A' : Type u_1
B' : Type u_2
a b : R
n : ℕ
inst✝⁵ : CommSemiring A'
inst✝⁴ : Semiring B'
inst✝³ : CommSemiring R
p q r : R[X]
inst✝² : Semiring A
inst✝¹ : Algebra R A
inst✝ : Nontrivial A
x : R
⊢ ¬coeff (↑C (↑(algebraMap R A) x)) 1 = coeff X 1
[PROOFSTEP]
simp [coeff_C]
[GOAL]
R✝ : Type u
S : Type v
T : Type w
A✝ : Type z
A' : Type u_1
B' : Type u_2
a✝ b : R✝
n : ℕ
inst✝⁹ : CommSemiring A'
inst✝⁸ : Semiring B'
inst✝⁷ : CommSemiring R✝
p✝ q r : R✝[X]
inst✝⁶ : Semiring A✝
inst✝⁵ : Algebra R✝ A✝
R : Type u_3
A : Type u_4
B : Type u_5
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
p : R[X]
f : A →ₐ[R] B
a : A
⊢ ↑f (eval₂ (algebraMap R A) a p) = eval₂ (algebraMap R B) (↑f a) p
[PROOFSTEP]
simp only [eval₂_eq_sum, sum_def]
[GOAL]
R✝ : Type u
S : Type v
T : Type w
A✝ : Type z
A' : Type u_1
B' : Type u_2
a✝ b : R✝
n : ℕ
inst✝⁹ : CommSemiring A'
inst✝⁸ : Semiring B'
inst✝⁷ : CommSemiring R✝
p✝ q r : R✝[X]
inst✝⁶ : Semiring A✝
inst✝⁵ : Algebra R✝ A✝
R : Type u_3
A : Type u_4
B : Type u_5
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
p : R[X]
f : A →ₐ[R] B
a : A
⊢ ↑f (∑ n in support p, ↑(algebraMap R A) (coeff p n) * a ^ n) =
    ∑ n in support p, ↑(algebraMap R B) (coeff p n) * ↑f a ^ n
[PROOFSTEP]
simp only [f.map_sum, f.map_mul, f.map_pow, eq_intCast, map_intCast, AlgHom.commutes]
[GOAL]
R✝ : Type u
S : Type v
T : Type w
A✝ : Type z
A' : Type u_1
B' : Type u_2
a b : R✝
n : ℕ
inst✝⁷ : CommSemiring A'
inst✝⁶ : Semiring B'
inst✝⁵ : CommSemiring R✝
p✝ q r : R✝[X]
inst✝⁴ : Semiring A✝
inst✝³ : Algebra R✝ A✝
R : Type u_3
A : Type u_4
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
p : R[X]
f : R[X] →ₐ[R] A
⊢ eval₂ (algebraMap R A) (↑f X) p = ↑f p
[PROOFSTEP]
conv_rhs => rw [← Polynomial.sum_C_mul_X_pow_eq p]
[GOAL]
R✝ : Type u
S : Type v
T : Type w
A✝ : Type z
A' : Type u_1
B' : Type u_2
a b : R✝
n : ℕ
inst✝⁷ : CommSemiring A'
inst✝⁶ : Semiring B'
inst✝⁵ : CommSemiring R✝
p✝ q r : R✝[X]
inst✝⁴ : Semiring A✝
inst✝³ : Algebra R✝ A✝
R : Type u_3
A : Type u_4
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
p : R[X]
f : R[X] →ₐ[R] A
| ↑f p
[PROOFSTEP]
rw [← Polynomial.sum_C_mul_X_pow_eq p]
[GOAL]
R✝ : Type u
S : Type v
T : Type w
A✝ : Type z
A' : Type u_1
B' : Type u_2
a b : R✝
n : ℕ
inst✝⁷ : CommSemiring A'
inst✝⁶ : Semiring B'
inst✝⁵ : CommSemiring R✝
p✝ q r : R✝[X]
inst✝⁴ : Semiring A✝
inst✝³ : Algebra R✝ A✝
R : Type u_3
A : Type u_4
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
p : R[X]
f : R[X] →ₐ[R] A
| ↑f p
[PROOFSTEP]
rw [← Polynomial.sum_C_mul_X_pow_eq p]
[GOAL]
R✝ : Type u
S : Type v
T : Type w
A✝ : Type z
A' : Type u_1
B' : Type u_2
a b : R✝
n : ℕ
inst✝⁷ : CommSemiring A'
inst✝⁶ : Semiring B'
inst✝⁵ : CommSemiring R✝
p✝ q r : R✝[X]
inst✝⁴ : Semiring A✝
inst✝³ : Algebra R✝ A✝
R : Type u_3
A : Type u_4
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
p : R[X]
f : R[X] →ₐ[R] A
| ↑f p
[PROOFSTEP]
rw [← Polynomial.sum_C_mul_X_pow_eq p]
[GOAL]
R✝ : Type u
S : Type v
T : Type w
A✝ : Type z
A' : Type u_1
B' : Type u_2
a b : R✝
n : ℕ
inst✝⁷ : CommSemiring A'
inst✝⁶ : Semiring B'
inst✝⁵ : CommSemiring R✝
p✝ q r : R✝[X]
inst✝⁴ : Semiring A✝
inst✝³ : Algebra R✝ A✝
R : Type u_3
A : Type u_4
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
p : R[X]
f : R[X] →ₐ[R] A
⊢ eval₂ (algebraMap R A) (↑f X) p = ↑f (sum p fun n a => ↑C a * X ^ n)
[PROOFSTEP]
simp only [eval₂_eq_sum, sum_def]
[GOAL]
R✝ : Type u
S : Type v
T : Type w
A✝ : Type z
A' : Type u_1
B' : Type u_2
a b : R✝
n : ℕ
inst✝⁷ : CommSemiring A'
inst✝⁶ : Semiring B'
inst✝⁵ : CommSemiring R✝
p✝ q r : R✝[X]
inst✝⁴ : Semiring A✝
inst✝³ : Algebra R✝ A✝
R : Type u_3
A : Type u_4
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
p : R[X]
f : R[X] →ₐ[R] A
⊢ ∑ n in support p, ↑(algebraMap R A) (coeff p n) * ↑f X ^ n = ↑f (∑ n in support p, ↑C (coeff p n) * X ^ n)
[PROOFSTEP]
simp only [f.map_sum, f.map_mul, f.map_pow, eq_intCast, map_intCast]
[GOAL]
R✝ : Type u
S : Type v
T : Type w
A✝ : Type z
A' : Type u_1
B' : Type u_2
a b : R✝
n : ℕ
inst✝⁷ : CommSemiring A'
inst✝⁶ : Semiring B'
inst✝⁵ : CommSemiring R✝
p✝ q r : R✝[X]
inst✝⁴ : Semiring A✝
inst✝³ : Algebra R✝ A✝
R : Type u_3
A : Type u_4
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
p : R[X]
f : R[X] →ₐ[R] A
⊢ ∑ n in support p, ↑(algebraMap R A) (coeff p n) * ↑f X ^ n = ∑ x in support p, ↑f (↑C (coeff p x)) * ↑f X ^ x
[PROOFSTEP]
simp [Polynomial.C_eq_algebraMap]
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
A' : Type u_1
B' : Type u_2
a b : R
n : ℕ
inst✝⁶ : CommSemiring A'
inst✝⁵ : Semiring B'
inst✝⁴ : CommSemiring R
p q : R[X]
inst✝³ : Semiring A
inst✝² : Algebra R A
B : Type u_3
inst✝¹ : Semiring B
inst✝ : Algebra R B
x : A
⊢ Algebra.adjoin R {X} = ⊤
[PROOFSTEP]
refine' top_unique fun p _hp => _
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
A' : Type u_1
B' : Type u_2
a b : R
n : ℕ
inst✝⁶ : CommSemiring A'
inst✝⁵ : Semiring B'
inst✝⁴ : CommSemiring R
p✝ q : R[X]
inst✝³ : Semiring A
inst✝² : Algebra R A
B : Type u_3
inst✝¹ : Semiring B
inst✝ : Algebra R B
x : A
p : R[X]
_hp : p ∈ ⊤
⊢ p ∈ Algebra.adjoin R {X}
[PROOFSTEP]
set S := Algebra.adjoin R ({ X } : Set R[X])
[GOAL]
R : Type u
S✝ : Type v
T : Type w
A : Type z
A' : Type u_1
B' : Type u_2
a b : R
n : ℕ
inst✝⁶ : CommSemiring A'
inst✝⁵ : Semiring B'
inst✝⁴ : CommSemiring R
p✝ q : R[X]
inst✝³ : Semiring A
inst✝² : Algebra R A
B : Type u_3
inst✝¹ : Semiring B
inst✝ : Algebra R B
x : A
p : R[X]
_hp : p ∈ ⊤
S : Subalgebra R R[X] := Algebra.adjoin R {X}
⊢ p ∈ S
[PROOFSTEP]
rw [← sum_monomial_eq p]
[GOAL]
R : Type u
S✝ : Type v
T : Type w
A : Type z
A' : Type u_1
B' : Type u_2
a b : R
n : ℕ
inst✝⁶ : CommSemiring A'
inst✝⁵ : Semiring B'
inst✝⁴ : CommSemiring R
p✝ q : R[X]
inst✝³ : Semiring A
inst✝² : Algebra R A
B : Type u_3
inst✝¹ : Semiring B
inst✝ : Algebra R B
x : A
p : R[X]
_hp : p ∈ ⊤
S : Subalgebra R R[X] := Algebra.adjoin R {X}
⊢ (sum p fun n a => ↑(monomial n) a) ∈ S
[PROOFSTEP]
simp only [← smul_X_eq_monomial, Sum]
[GOAL]
R : Type u
S✝ : Type v
T : Type w
A : Type z
A' : Type u_1
B' : Type u_2
a b : R
n : ℕ
inst✝⁶ : CommSemiring A'
inst✝⁵ : Semiring B'
inst✝⁴ : CommSemiring R
p✝ q : R[X]
inst✝³ : Semiring A
inst✝² : Algebra R A
B : Type u_3
inst✝¹ : Semiring B
inst✝ : Algebra R B
x : A
p : R[X]
_hp : p ∈ ⊤
S : Subalgebra R R[X] := Algebra.adjoin R {X}
⊢ (sum p fun n a => a • X ^ n) ∈ Algebra.adjoin R {X}
[PROOFSTEP]
exact S.sum_mem fun n _hn => S.smul_mem (S.pow_mem (Algebra.subset_adjoin rfl) _) _
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
A' : Type u_1
B' : Type u_2
a b : R
n : ℕ
inst✝⁶ : CommSemiring A'
inst✝⁵ : Semiring B'
inst✝⁴ : CommSemiring R
p q : R[X]
inst✝³ : Semiring A
inst✝² : Algebra R A
B : Type u_3
inst✝¹ : Semiring B
inst✝ : Algebra R B
x✝ : A
f : A →ₐ[R] B
x : A
⊢ ↑(aeval (↑f x)) X = ↑(AlgHom.comp f (aeval x)) X
[PROOFSTEP]
simp only [aeval_X, AlgHom.comp_apply]
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
A' : Type u_1
B' : Type u_2
a b : R
n : ℕ
inst✝⁶ : CommSemiring A'
inst✝⁵ : Semiring B'
inst✝⁴ : CommSemiring R
p✝ q : R[X]
inst✝³ : Semiring A
inst✝² : Algebra R A
B : Type u_3
inst✝¹ : Semiring B
inst✝ : Algebra R B
x : A
φ : R[X] →ₐ[R] A
p : R[X]
⊢ ↑φ p = eval₂ (algebraMap R A) (↑φ X) p
[PROOFSTEP]
rw [← aeval_def, aeval_algHom, aeval_X_left, AlgHom.comp_id]
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
A' : Type u_1
B' : Type u_2
a b : R
n : ℕ
inst✝⁷ : CommSemiring A'
inst✝⁶ : Semiring B'
inst✝⁵ : CommSemiring R
p✝ q : R[X]
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
B : Type u_3
inst✝² : Semiring B
inst✝¹ : Algebra R B
x✝ : A
F : Type u_4
inst✝ : AlgHomClass F R A B
f : F
x : A
p : R[X]
⊢ ↑(aeval (↑f x)) p = ↑f (↑(aeval x) p)
[PROOFSTEP]
refine' Polynomial.induction_on p (by simp [AlgHomClass.commutes]) (fun p q hp hq => _) (by simp [AlgHomClass.commutes])
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
A' : Type u_1
B' : Type u_2
a b : R
n : ℕ
inst✝⁷ : CommSemiring A'
inst✝⁶ : Semiring B'
inst✝⁵ : CommSemiring R
p✝ q : R[X]
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
B : Type u_3
inst✝² : Semiring B
inst✝¹ : Algebra R B
x✝ : A
F : Type u_4
inst✝ : AlgHomClass F R A B
f : F
x : A
p : R[X]
⊢ ∀ (a : R), ↑(aeval (↑f x)) (↑C a) = ↑f (↑(aeval x) (↑C a))
[PROOFSTEP]
simp [AlgHomClass.commutes]
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
A' : Type u_1
B' : Type u_2
a b : R
n : ℕ
inst✝⁷ : CommSemiring A'
inst✝⁶ : Semiring B'
inst✝⁵ : CommSemiring R
p✝ q : R[X]
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
B : Type u_3
inst✝² : Semiring B
inst✝¹ : Algebra R B
x✝ : A
F : Type u_4
inst✝ : AlgHomClass F R A B
f : F
x : A
p : R[X]
⊢ ∀ (n : ℕ) (a : R),
    ↑(aeval (↑f x)) (↑C a * X ^ n) = ↑f (↑(aeval x) (↑C a * X ^ n)) →
      ↑(aeval (↑f x)) (↑C a * X ^ (n + 1)) = ↑f (↑(aeval x) (↑C a * X ^ (n + 1)))
[PROOFSTEP]
simp [AlgHomClass.commutes]
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
A' : Type u_1
B' : Type u_2
a b : R
n : ℕ
inst✝⁷ : CommSemiring A'
inst✝⁶ : Semiring B'
inst✝⁵ : CommSemiring R
p✝¹ q✝ : R[X]
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
B : Type u_3
inst✝² : Semiring B
inst✝¹ : Algebra R B
x✝ : A
F : Type u_4
inst✝ : AlgHomClass F R A B
f : F
x : A
p✝ p q : R[X]
hp : ↑(aeval (↑f x)) p = ↑f (↑(aeval x) p)
hq : ↑(aeval (↑f x)) q = ↑f (↑(aeval x) q)
⊢ ↑(aeval (↑f x)) (p + q) = ↑f (↑(aeval x) (p + q))
[PROOFSTEP]
rw [map_add, hp, hq, ← map_add, ← map_add]
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
A' : Type u_1
B' : Type u_2
a b : R
n : ℕ
inst✝⁶ : CommSemiring A'
inst✝⁵ : Semiring B'
inst✝⁴ : CommSemiring R
p✝ q : R[X]
inst✝³ : Semiring A
inst✝² : Algebra R A
B : Type u_3
inst✝¹ : Semiring B
inst✝ : Algebra R B
x : A
p : R[X]
⊢ coeff p 0 = ↑(aeval 0) p
[PROOFSTEP]
simp [coeff_zero_eq_eval_zero]
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
A' : Type u_1
B' : Type u_2
a b : R
n : ℕ
inst✝⁶ : CommSemiring A'
inst✝⁵ : Semiring B'
inst✝⁴ : CommSemiring R
p✝ q : R[X]
inst✝³ : Semiring A
inst✝² : Algebra R A
B : Type u_3
inst✝¹ : Semiring B
inst✝ : Algebra R B
x : A
p : R[X]
⊢ ↑(algebraMap R A) (coeff p 0) = ↑(aeval 0) p
[PROOFSTEP]
simp [aeval_def]
[GOAL]
R : Type u
S✝ : Type v
T✝ : Type w
A : Type z
A' : Type u_1
B' : Type u_2
a✝ b : R
n : ℕ
inst✝¹¹ : CommSemiring A'
inst✝¹⁰ : Semiring B'
inst✝⁹ : CommSemiring R
p✝ q : R[X]
inst✝⁸ : Semiring A
inst✝⁷ : Algebra R A
B : Type u_3
inst✝⁶ : Semiring B
inst✝⁵ : Algebra R B
x : A
S : Type u_4
T : Type u_5
U : Type u_6
inst✝⁴ : CommSemiring S
inst✝³ : CommSemiring T
inst✝² : Semiring U
inst✝¹ : Algebra R S
inst✝ : Algebra T U
φ : R →+* T
ψ : S →+* U
h : RingHom.comp (algebraMap T U) φ = RingHom.comp ψ (algebraMap R S)
p : R[X]
a : S
⊢ ↑ψ (↑(aeval a) p) = ↑(aeval (↑ψ a)) (map φ p)
[PROOFSTEP]
conv_rhs => rw [aeval_def, ← eval_map]
[GOAL]
R : Type u
S✝ : Type v
T✝ : Type w
A : Type z
A' : Type u_1
B' : Type u_2
a✝ b : R
n : ℕ
inst✝¹¹ : CommSemiring A'
inst✝¹⁰ : Semiring B'
inst✝⁹ : CommSemiring R
p✝ q : R[X]
inst✝⁸ : Semiring A
inst✝⁷ : Algebra R A
B : Type u_3
inst✝⁶ : Semiring B
inst✝⁵ : Algebra R B
x : A
S : Type u_4
T : Type u_5
U : Type u_6
inst✝⁴ : CommSemiring S
inst✝³ : CommSemiring T
inst✝² : Semiring U
inst✝¹ : Algebra R S
inst✝ : Algebra T U
φ : R →+* T
ψ : S →+* U
h : RingHom.comp (algebraMap T U) φ = RingHom.comp ψ (algebraMap R S)
p : R[X]
a : S
| ↑(aeval (↑ψ a)) (map φ p)
[PROOFSTEP]
rw [aeval_def, ← eval_map]
[GOAL]
R : Type u
S✝ : Type v
T✝ : Type w
A : Type z
A' : Type u_1
B' : Type u_2
a✝ b : R
n : ℕ
inst✝¹¹ : CommSemiring A'
inst✝¹⁰ : Semiring B'
inst✝⁹ : CommSemiring R
p✝ q : R[X]
inst✝⁸ : Semiring A
inst✝⁷ : Algebra R A
B : Type u_3
inst✝⁶ : Semiring B
inst✝⁵ : Algebra R B
x : A
S : Type u_4
T : Type u_5
U : Type u_6
inst✝⁴ : CommSemiring S
inst✝³ : CommSemiring T
inst✝² : Semiring U
inst✝¹ : Algebra R S
inst✝ : Algebra T U
φ : R →+* T
ψ : S →+* U
h : RingHom.comp (algebraMap T U) φ = RingHom.comp ψ (algebraMap R S)
p : R[X]
a : S
| ↑(aeval (↑ψ a)) (map φ p)
[PROOFSTEP]
rw [aeval_def, ← eval_map]
[GOAL]
R : Type u
S✝ : Type v
T✝ : Type w
A : Type z
A' : Type u_1
B' : Type u_2
a✝ b : R
n : ℕ
inst✝¹¹ : CommSemiring A'
inst✝¹⁰ : Semiring B'
inst✝⁹ : CommSemiring R
p✝ q : R[X]
inst✝⁸ : Semiring A
inst✝⁷ : Algebra R A
B : Type u_3
inst✝⁶ : Semiring B
inst✝⁵ : Algebra R B
x : A
S : Type u_4
T : Type u_5
U : Type u_6
inst✝⁴ : CommSemiring S
inst✝³ : CommSemiring T
inst✝² : Semiring U
inst✝¹ : Algebra R S
inst✝ : Algebra T U
φ : R →+* T
ψ : S →+* U
h : RingHom.comp (algebraMap T U) φ = RingHom.comp ψ (algebraMap R S)
p : R[X]
a : S
| ↑(aeval (↑ψ a)) (map φ p)
[PROOFSTEP]
rw [aeval_def, ← eval_map]
[GOAL]
R : Type u
S✝ : Type v
T✝ : Type w
A : Type z
A' : Type u_1
B' : Type u_2
a✝ b : R
n : ℕ
inst✝¹¹ : CommSemiring A'
inst✝¹⁰ : Semiring B'
inst✝⁹ : CommSemiring R
p✝ q : R[X]
inst✝⁸ : Semiring A
inst✝⁷ : Algebra R A
B : Type u_3
inst✝⁶ : Semiring B
inst✝⁵ : Algebra R B
x : A
S : Type u_4
T : Type u_5
U : Type u_6
inst✝⁴ : CommSemiring S
inst✝³ : CommSemiring T
inst✝² : Semiring U
inst✝¹ : Algebra R S
inst✝ : Algebra T U
φ : R →+* T
ψ : S →+* U
h : RingHom.comp (algebraMap T U) φ = RingHom.comp ψ (algebraMap R S)
p : R[X]
a : S
⊢ ↑ψ (↑(aeval a) p) = eval (↑ψ a) (map (algebraMap T ((fun x => U) a)) (map φ p))
[PROOFSTEP]
rw [map_map, h, ← map_map, eval_map, eval₂_at_apply, aeval_def, eval_map]
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
A' : Type u_1
B' : Type u_2
a✝ b : R
n : ℕ
inst✝⁹ : CommSemiring A'
inst✝⁸ : Semiring B'
inst✝⁷ : CommSemiring R
p✝ q✝ : R[X]
inst✝⁶ : Semiring A
inst✝⁵ : Algebra R A
B : Type u_3
inst✝⁴ : Semiring B
inst✝³ : Algebra R B
x : A
inst✝² : CommSemiring S
inst✝¹ : CommSemiring T
inst✝ : Algebra S T
p q : S[X]
h₁ : p ∣ q
a : T
h₂ : ↑(aeval a) p = 0
⊢ ↑(aeval a) q = 0
[PROOFSTEP]
rw [aeval_def, ← eval_map] at h₂ ⊢
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
A' : Type u_1
B' : Type u_2
a✝ b : R
n : ℕ
inst✝⁹ : CommSemiring A'
inst✝⁸ : Semiring B'
inst✝⁷ : CommSemiring R
p✝ q✝ : R[X]
inst✝⁶ : Semiring A
inst✝⁵ : Algebra R A
B : Type u_3
inst✝⁴ : Semiring B
inst✝³ : Algebra R B
x : A
inst✝² : CommSemiring S
inst✝¹ : CommSemiring T
inst✝ : Algebra S T
p q : S[X]
h₁ : p ∣ q
a : T
h₂ : eval a (map (algebraMap S T) p) = 0
⊢ eval a (map (algebraMap S T) q) = 0
[PROOFSTEP]
exact eval_eq_zero_of_dvd_of_eval_eq_zero (Polynomial.map_dvd (algebraMap S T) h₁) h₂
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
A' : Type u_1
B' : Type u_2
a b : R
n : ℕ
inst✝⁶ : CommSemiring A'
inst✝⁵ : Semiring B'
inst✝⁴ : CommSemiring R
p q : R[X]
inst✝³ : Semiring A
inst✝² : Algebra R A
B : Type u_3
inst✝¹ : Semiring B
inst✝ : Algebra R B
x✝ x : A
⊢ Algebra.adjoin R {x} = AlgHom.range (aeval x)
[PROOFSTEP]
rw [← Algebra.map_top, ← adjoin_X, AlgHom.map_adjoin, Set.image_singleton, aeval_X]
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
A' : Type u_1
B' : Type u_2
a b : R
n : ℕ
inst✝⁸ : CommSemiring A'
inst✝⁷ : Semiring B'
inst✝⁶ : CommSemiring R
p✝ q : R[X]
inst✝⁵ : Semiring A
inst✝⁴ : Algebra R A
B : Type u_3
inst✝³ : Semiring B
inst✝² : Algebra R B
x✝ : A
inst✝¹ : Semiring S
f : R →+* S
inst✝ : Algebra R S
p : R[X]
x : S
⊢ ↑(aeval x) p = ∑ i in range (natDegree p + 1), coeff p i • x ^ i
[PROOFSTEP]
simp_rw [Algebra.smul_def]
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
A' : Type u_1
B' : Type u_2
a b : R
n : ℕ
inst✝⁸ : CommSemiring A'
inst✝⁷ : Semiring B'
inst✝⁶ : CommSemiring R
p✝ q : R[X]
inst✝⁵ : Semiring A
inst✝⁴ : Algebra R A
B : Type u_3
inst✝³ : Semiring B
inst✝² : Algebra R B
x✝ : A
inst✝¹ : Semiring S
f : R →+* S
inst✝ : Algebra R S
p : R[X]
x : S
⊢ ↑(aeval x) p = ∑ x_1 in range (natDegree p + 1), ↑(algebraMap R S) (coeff p x_1) * x ^ x_1
[PROOFSTEP]
exact eval₂_eq_sum_range (algebraMap R S) x
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
A' : Type u_1
B' : Type u_2
a b : R
n✝ : ℕ
inst✝⁸ : CommSemiring A'
inst✝⁷ : Semiring B'
inst✝⁶ : CommSemiring R
p✝ q : R[X]
inst✝⁵ : Semiring A
inst✝⁴ : Algebra R A
B : Type u_3
inst✝³ : Semiring B
inst✝² : Algebra R B
x✝ : A
inst✝¹ : Semiring S
f : R →+* S
inst✝ : Algebra R S
p : R[X]
n : ℕ
hn : natDegree p < n
x : S
⊢ ↑(aeval x) p = ∑ i in range n, coeff p i • x ^ i
[PROOFSTEP]
simp_rw [Algebra.smul_def]
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
A' : Type u_1
B' : Type u_2
a b : R
n✝ : ℕ
inst✝⁸ : CommSemiring A'
inst✝⁷ : Semiring B'
inst✝⁶ : CommSemiring R
p✝ q : R[X]
inst✝⁵ : Semiring A
inst✝⁴ : Algebra R A
B : Type u_3
inst✝³ : Semiring B
inst✝² : Algebra R B
x✝ : A
inst✝¹ : Semiring S
f : R →+* S
inst✝ : Algebra R S
p : R[X]
n : ℕ
hn : natDegree p < n
x : S
⊢ ↑(aeval x) p = ∑ x_1 in range n, ↑(algebraMap R S) (coeff p x_1) * x ^ x_1
[PROOFSTEP]
exact eval₂_eq_sum_range' (algebraMap R S) hn x
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
A' : Type u_1
B' : Type u_2
a b : R
n : ℕ
inst✝⁷ : CommSemiring A'
inst✝⁶ : Semiring B'
inst✝⁵ : CommSemiring R
p q : R[X]
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
B : Type u_3
inst✝² : Semiring B
inst✝¹ : Algebra R B
x : A
inst✝ : Semiring S
f : R →+* S
hf : Function.Injective ↑f
r : R
⊢ eval₂ f (↑f r) p = 0 → IsRoot p r
[PROOFSTEP]
intro h
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
A' : Type u_1
B' : Type u_2
a b : R
n : ℕ
inst✝⁷ : CommSemiring A'
inst✝⁶ : Semiring B'
inst✝⁵ : CommSemiring R
p q : R[X]
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
B : Type u_3
inst✝² : Semiring B
inst✝¹ : Algebra R B
x : A
inst✝ : Semiring S
f : R →+* S
hf : Function.Injective ↑f
r : R
h : eval₂ f (↑f r) p = 0
⊢ IsRoot p r
[PROOFSTEP]
apply hf
[GOAL]
case a
R : Type u
S : Type v
T : Type w
A : Type z
A' : Type u_1
B' : Type u_2
a b : R
n : ℕ
inst✝⁷ : CommSemiring A'
inst✝⁶ : Semiring B'
inst✝⁵ : CommSemiring R
p q : R[X]
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
B : Type u_3
inst✝² : Semiring B
inst✝¹ : Algebra R B
x : A
inst✝ : Semiring S
f : R →+* S
hf : Function.Injective ↑f
r : R
h : eval₂ f (↑f r) p = 0
⊢ ↑f (eval r p) = ↑f 0
[PROOFSTEP]
rw [← eval₂_hom, h, f.map_zero]
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
A' : Type u_1
B' : Type u_2
a b : R
n : ℕ
inst✝¹⁰ : CommSemiring A'
inst✝⁹ : Semiring B'
inst✝⁸ : CommSemiring R
p q : R[X]
inst✝⁷ : Semiring A
inst✝⁶ : Algebra R A
B : Type u_3
inst✝⁵ : Semiring B
inst✝⁴ : Algebra R B
x✝ : A
inst✝³ : CommSemiring S
inst✝² : Algebra S R
inst✝¹ : Algebra S A'
inst✝ : Algebra S B'
f : R →ₐ[S] A'
x : A'
src✝ : R[X] →+* A' := eval₂RingHom (↑f) x
r : S
⊢ OneHom.toFun
      (↑↑{ toMonoidHom := ↑src✝, map_zero' := (_ : OneHom.toFun (↑↑src✝) 0 = 0),
            map_add' :=
              (_ : ∀ (x y : R[X]), OneHom.toFun (↑↑src✝) (x + y) = OneHom.toFun (↑↑src✝) x + OneHom.toFun (↑↑src✝) y) })
      (↑(algebraMap S R[X]) r) =
    ↑(algebraMap S A') r
[PROOFSTEP]
simp [algebraMap_apply]
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
A' : Type u_1
B' : Type u_2
a b : R
n : ℕ
inst✝¹⁰ : CommSemiring A'
inst✝⁹ : Semiring B'
inst✝⁸ : CommSemiring R
p q : R[X]
inst✝⁷ : Semiring A
inst✝⁶ : Algebra R A
B : Type u_3
inst✝⁵ : Semiring B
inst✝⁴ : Algebra R B
x : A
inst✝³ : CommSemiring S
inst✝² : Algebra S R
inst✝¹ : Algebra S A'
inst✝ : Algebra S B'
g : R →ₐ[S] A'
y : A'
⊢ aevalTower (AlgHom.id S S) = aeval
[PROOFSTEP]
ext s
[GOAL]
case h.h
R : Type u
S : Type v
T : Type w
A : Type z
A' : Type u_1
B' : Type u_2
a b : R
n : ℕ
inst✝¹⁰ : CommSemiring A'
inst✝⁹ : Semiring B'
inst✝⁸ : CommSemiring R
p q : R[X]
inst✝⁷ : Semiring A
inst✝⁶ : Algebra R A
B : Type u_3
inst✝⁵ : Semiring B
inst✝⁴ : Algebra R B
x : A
inst✝³ : CommSemiring S
inst✝² : Algebra S R
inst✝¹ : Algebra S A'
inst✝ : Algebra S B'
g : R →ₐ[S] A'
y : A'
s : S
⊢ ↑(aevalTower (AlgHom.id S S) s) X = ↑(aeval s) X
[PROOFSTEP]
simp only [eval_X, aevalTower_X, coe_aeval_eq_eval]
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
A' : Type u_1
B' : Type u_2
a b : R
n : ℕ
inst✝¹⁰ : CommSemiring A'
inst✝⁹ : Semiring B'
inst✝⁸ : CommSemiring R
p q : R[X]
inst✝⁷ : Semiring A
inst✝⁶ : Algebra R A
B : Type u_3
inst✝⁵ : Semiring B
inst✝⁴ : Algebra R B
x : A
inst✝³ : CommSemiring S
inst✝² : Algebra S R
inst✝¹ : Algebra S A'
inst✝ : Algebra S B'
g : R →ₐ[S] A'
y : A'
⊢ aevalTower (Algebra.ofId S A') = aeval
[PROOFSTEP]
ext
[GOAL]
case h.h
R : Type u
S : Type v
T : Type w
A : Type z
A' : Type u_1
B' : Type u_2
a b : R
n : ℕ
inst✝¹⁰ : CommSemiring A'
inst✝⁹ : Semiring B'
inst✝⁸ : CommSemiring R
p q : R[X]
inst✝⁷ : Semiring A
inst✝⁶ : Algebra R A
B : Type u_3
inst✝⁵ : Semiring B
inst✝⁴ : Algebra R B
x : A
inst✝³ : CommSemiring S
inst✝² : Algebra S R
inst✝¹ : Algebra S A'
inst✝ : Algebra S B'
g : R →ₐ[S] A'
y x✝ : A'
⊢ ↑(aevalTower (Algebra.ofId S A') x✝) X = ↑(aeval x✝) X
[PROOFSTEP]
simp only [aeval_X, aevalTower_X]
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
A' : Type u_1
B' : Type u_2
a b : R
n : ℕ
inst✝⁷ : CommSemiring A'
inst✝⁶ : Semiring B'
inst✝⁵ : CommSemiring R
p✝ q : R[X]
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
B : Type u_3
inst✝² : Semiring B
inst✝¹ : Algebra R B
x : A
inst✝ : CommRing S
f✝ : R →+* S
z p : S
f : S[X]
i : ℕ
dvd_eval : p ∣ eval z f
dvd_terms : ∀ (j : ℕ), j ≠ i → p ∣ coeff f j * z ^ j
⊢ p ∣ coeff f i * z ^ i
[PROOFSTEP]
by_cases hi : i ∈ f.support
[GOAL]
case pos
R : Type u
S : Type v
T : Type w
A : Type z
A' : Type u_1
B' : Type u_2
a b : R
n : ℕ
inst✝⁷ : CommSemiring A'
inst✝⁶ : Semiring B'
inst✝⁵ : CommSemiring R
p✝ q : R[X]
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
B : Type u_3
inst✝² : Semiring B
inst✝¹ : Algebra R B
x : A
inst✝ : CommRing S
f✝ : R →+* S
z p : S
f : S[X]
i : ℕ
dvd_eval : p ∣ eval z f
dvd_terms : ∀ (j : ℕ), j ≠ i → p ∣ coeff f j * z ^ j
hi : i ∈ support f
⊢ p ∣ coeff f i * z ^ i
[PROOFSTEP]
rw [eval, eval₂_eq_sum, sum_def] at dvd_eval 
[GOAL]
case pos
R : Type u
S : Type v
T : Type w
A : Type z
A' : Type u_1
B' : Type u_2
a b : R
n : ℕ
inst✝⁷ : CommSemiring A'
inst✝⁶ : Semiring B'
inst✝⁵ : CommSemiring R
p✝ q : R[X]
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
B : Type u_3
inst✝² : Semiring B
inst✝¹ : Algebra R B
x : A
inst✝ : CommRing S
f✝ : R →+* S
z p : S
f : S[X]
i : ℕ
dvd_eval : p ∣ ∑ n in support f, ↑(RingHom.id S) (coeff f n) * z ^ n
dvd_terms : ∀ (j : ℕ), j ≠ i → p ∣ coeff f j * z ^ j
hi : i ∈ support f
⊢ p ∣ coeff f i * z ^ i
[PROOFSTEP]
rw [← Finset.insert_erase hi, Finset.sum_insert (Finset.not_mem_erase _ _)] at dvd_eval 
[GOAL]
case pos
R : Type u
S : Type v
T : Type w
A : Type z
A' : Type u_1
B' : Type u_2
a b : R
n : ℕ
inst✝⁷ : CommSemiring A'
inst✝⁶ : Semiring B'
inst✝⁵ : CommSemiring R
p✝ q : R[X]
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
B : Type u_3
inst✝² : Semiring B
inst✝¹ : Algebra R B
x : A
inst✝ : CommRing S
f✝ : R →+* S
z p : S
f : S[X]
i : ℕ
dvd_eval :
  p ∣ ↑(RingHom.id S) (coeff f i) * z ^ i + ∑ x in Finset.erase (support f) i, ↑(RingHom.id S) (coeff f x) * z ^ x
dvd_terms : ∀ (j : ℕ), j ≠ i → p ∣ coeff f j * z ^ j
hi : i ∈ support f
⊢ p ∣ coeff f i * z ^ i
[PROOFSTEP]
refine' (dvd_add_left _).mp dvd_eval
[GOAL]
case pos
R : Type u
S : Type v
T : Type w
A : Type z
A' : Type u_1
B' : Type u_2
a b : R
n : ℕ
inst✝⁷ : CommSemiring A'
inst✝⁶ : Semiring B'
inst✝⁵ : CommSemiring R
p✝ q : R[X]
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
B : Type u_3
inst✝² : Semiring B
inst✝¹ : Algebra R B
x : A
inst✝ : CommRing S
f✝ : R →+* S
z p : S
f : S[X]
i : ℕ
dvd_eval :
  p ∣ ↑(RingHom.id S) (coeff f i) * z ^ i + ∑ x in Finset.erase (support f) i, ↑(RingHom.id S) (coeff f x) * z ^ x
dvd_terms : ∀ (j : ℕ), j ≠ i → p ∣ coeff f j * z ^ j
hi : i ∈ support f
⊢ p ∣ ∑ x in Finset.erase (support f) i, ↑(RingHom.id S) (coeff f x) * z ^ x
[PROOFSTEP]
apply Finset.dvd_sum
[GOAL]
case pos.h
R : Type u
S : Type v
T : Type w
A : Type z
A' : Type u_1
B' : Type u_2
a b : R
n : ℕ
inst✝⁷ : CommSemiring A'
inst✝⁶ : Semiring B'
inst✝⁵ : CommSemiring R
p✝ q : R[X]
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
B : Type u_3
inst✝² : Semiring B
inst✝¹ : Algebra R B
x : A
inst✝ : CommRing S
f✝ : R →+* S
z p : S
f : S[X]
i : ℕ
dvd_eval :
  p ∣ ↑(RingHom.id S) (coeff f i) * z ^ i + ∑ x in Finset.erase (support f) i, ↑(RingHom.id S) (coeff f x) * z ^ x
dvd_terms : ∀ (j : ℕ), j ≠ i → p ∣ coeff f j * z ^ j
hi : i ∈ support f
⊢ ∀ (x : ℕ), x ∈ Finset.erase (support f) i → p ∣ ↑(RingHom.id S) (coeff f x) * z ^ x
[PROOFSTEP]
intro j hj
[GOAL]
case pos.h
R : Type u
S : Type v
T : Type w
A : Type z
A' : Type u_1
B' : Type u_2
a b : R
n : ℕ
inst✝⁷ : CommSemiring A'
inst✝⁶ : Semiring B'
inst✝⁵ : CommSemiring R
p✝ q : R[X]
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
B : Type u_3
inst✝² : Semiring B
inst✝¹ : Algebra R B
x : A
inst✝ : CommRing S
f✝ : R →+* S
z p : S
f : S[X]
i : ℕ
dvd_eval :
  p ∣ ↑(RingHom.id S) (coeff f i) * z ^ i + ∑ x in Finset.erase (support f) i, ↑(RingHom.id S) (coeff f x) * z ^ x
dvd_terms : ∀ (j : ℕ), j ≠ i → p ∣ coeff f j * z ^ j
hi : i ∈ support f
j : ℕ
hj : j ∈ Finset.erase (support f) i
⊢ p ∣ ↑(RingHom.id S) (coeff f j) * z ^ j
[PROOFSTEP]
exact dvd_terms j (Finset.ne_of_mem_erase hj)
[GOAL]
case neg
R : Type u
S : Type v
T : Type w
A : Type z
A' : Type u_1
B' : Type u_2
a b : R
n : ℕ
inst✝⁷ : CommSemiring A'
inst✝⁶ : Semiring B'
inst✝⁵ : CommSemiring R
p✝ q : R[X]
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
B : Type u_3
inst✝² : Semiring B
inst✝¹ : Algebra R B
x : A
inst✝ : CommRing S
f✝ : R →+* S
z p : S
f : S[X]
i : ℕ
dvd_eval : p ∣ eval z f
dvd_terms : ∀ (j : ℕ), j ≠ i → p ∣ coeff f j * z ^ j
hi : ¬i ∈ support f
⊢ p ∣ coeff f i * z ^ i
[PROOFSTEP]
convert dvd_zero p
[GOAL]
case h.e'_4
R : Type u
S : Type v
T : Type w
A : Type z
A' : Type u_1
B' : Type u_2
a b : R
n : ℕ
inst✝⁷ : CommSemiring A'
inst✝⁶ : Semiring B'
inst✝⁵ : CommSemiring R
p✝ q : R[X]
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
B : Type u_3
inst✝² : Semiring B
inst✝¹ : Algebra R B
x : A
inst✝ : CommRing S
f✝ : R →+* S
z p : S
f : S[X]
i : ℕ
dvd_eval : p ∣ eval z f
dvd_terms : ∀ (j : ℕ), j ≠ i → p ∣ coeff f j * z ^ j
hi : ¬i ∈ support f
⊢ coeff f i * z ^ i = 0
[PROOFSTEP]
rw [not_mem_support_iff] at hi 
[GOAL]
case h.e'_4
R : Type u
S : Type v
T : Type w
A : Type z
A' : Type u_1
B' : Type u_2
a b : R
n : ℕ
inst✝⁷ : CommSemiring A'
inst✝⁶ : Semiring B'
inst✝⁵ : CommSemiring R
p✝ q : R[X]
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
B : Type u_3
inst✝² : Semiring B
inst✝¹ : Algebra R B
x : A
inst✝ : CommRing S
f✝ : R →+* S
z p : S
f : S[X]
i : ℕ
dvd_eval : p ∣ eval z f
dvd_terms : ∀ (j : ℕ), j ≠ i → p ∣ coeff f j * z ^ j
hi : coeff f i = 0
⊢ coeff f i * z ^ i = 0
[PROOFSTEP]
simp [hi]
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
A' : Type u_1
B' : Type u_2
a b : R
n : ℕ
inst✝² : CommSemiring A'
inst✝¹ : Semiring B'
inst✝ : Ring R
p : R[X]
r : R
⊢ eval r (p * (X - ↑C r)) = 0
[PROOFSTEP]
simp only [eval, eval₂_eq_sum, RingHom.id_apply]
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
A' : Type u_1
B' : Type u_2
a b : R
n : ℕ
inst✝² : CommSemiring A'
inst✝¹ : Semiring B'
inst✝ : Ring R
p : R[X]
r : R
⊢ (sum (p * (X - ↑C r)) fun e a => a * r ^ e) = 0
[PROOFSTEP]
have bound :=
  calc
    (p * (X - C r)).natDegree ≤ p.natDegree + (X - C r).natDegree := natDegree_mul_le
    _ ≤ p.natDegree + 1 := (add_le_add_left (natDegree_X_sub_C_le _) _)
    _ < p.natDegree + 2 := lt_add_one _
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
A' : Type u_1
B' : Type u_2
a b : R
n : ℕ
inst✝² : CommSemiring A'
inst✝¹ : Semiring B'
inst✝ : Ring R
p : R[X]
r : R
bound : natDegree (p * (X - ↑C r)) < natDegree p + 2
⊢ (sum (p * (X - ↑C r)) fun e a => a * r ^ e) = 0
[PROOFSTEP]
rw [sum_over_range' _ _ (p.natDegree + 2) bound]
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
A' : Type u_1
B' : Type u_2
a b : R
n : ℕ
inst✝² : CommSemiring A'
inst✝¹ : Semiring B'
inst✝ : Ring R
p : R[X]
r : R
bound : natDegree (p * (X - ↑C r)) < natDegree p + 2
⊢ ∑ a in range (natDegree p + 2), coeff (p * (X - ↑C r)) a * r ^ a = 0
R : Type u
S : Type v
T : Type w
A : Type z
A' : Type u_1
B' : Type u_2
a b : R
n : ℕ
inst✝² : CommSemiring A'
inst✝¹ : Semiring B'
inst✝ : Ring R
p : R[X]
r : R
bound : natDegree (p * (X - ↑C r)) < natDegree p + 2
⊢ ∀ (n : ℕ), 0 * r ^ n = 0
[PROOFSTEP]
swap
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
A' : Type u_1
B' : Type u_2
a b : R
n : ℕ
inst✝² : CommSemiring A'
inst✝¹ : Semiring B'
inst✝ : Ring R
p : R[X]
r : R
bound : natDegree (p * (X - ↑C r)) < natDegree p + 2
⊢ ∀ (n : ℕ), 0 * r ^ n = 0
[PROOFSTEP]
simp
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
A' : Type u_1
B' : Type u_2
a b : R
n : ℕ
inst✝² : CommSemiring A'
inst✝¹ : Semiring B'
inst✝ : Ring R
p : R[X]
r : R
bound : natDegree (p * (X - ↑C r)) < natDegree p + 2
⊢ ∑ a in range (natDegree p + 2), coeff (p * (X - ↑C r)) a * r ^ a = 0
[PROOFSTEP]
rw [sum_range_succ']
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
A' : Type u_1
B' : Type u_2
a b : R
n : ℕ
inst✝² : CommSemiring A'
inst✝¹ : Semiring B'
inst✝ : Ring R
p : R[X]
r : R
bound : natDegree (p * (X - ↑C r)) < natDegree p + 2
⊢ ∑ k in range (natDegree p + 1), coeff (p * (X - ↑C r)) (k + 1) * r ^ (k + 1) + coeff (p * (X - ↑C r)) 0 * r ^ 0 = 0
[PROOFSTEP]
conv_lhs =>
  congr
  arg 2
  simp [coeff_mul_X_sub_C, sub_mul, mul_assoc, ← pow_succ]
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
A' : Type u_1
B' : Type u_2
a b : R
n : ℕ
inst✝² : CommSemiring A'
inst✝¹ : Semiring B'
inst✝ : Ring R
p : R[X]
r : R
bound : natDegree (p * (X - ↑C r)) < natDegree p + 2
| ∑ k in range (natDegree p + 1), coeff (p * (X - ↑C r)) (k + 1) * r ^ (k + 1) + coeff (p * (X - ↑C r)) 0 * r ^ 0
[PROOFSTEP]
  congr
  arg 2
  simp [coeff_mul_X_sub_C, sub_mul, mul_assoc, ← pow_succ]
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
A' : Type u_1
B' : Type u_2
a b : R
n : ℕ
inst✝² : CommSemiring A'
inst✝¹ : Semiring B'
inst✝ : Ring R
p : R[X]
r : R
bound : natDegree (p * (X - ↑C r)) < natDegree p + 2
| ∑ k in range (natDegree p + 1), coeff (p * (X - ↑C r)) (k + 1) * r ^ (k + 1) + coeff (p * (X - ↑C r)) 0 * r ^ 0
[PROOFSTEP]
  congr
  arg 2
  simp [coeff_mul_X_sub_C, sub_mul, mul_assoc, ← pow_succ]
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
A' : Type u_1
B' : Type u_2
a b : R
n : ℕ
inst✝² : CommSemiring A'
inst✝¹ : Semiring B'
inst✝ : Ring R
p : R[X]
r : R
bound : natDegree (p * (X - ↑C r)) < natDegree p + 2
| ∑ k in range (natDegree p + 1), coeff (p * (X - ↑C r)) (k + 1) * r ^ (k + 1) + coeff (p * (X - ↑C r)) 0 * r ^ 0
[PROOFSTEP]
congr
[GOAL]
case a
R : Type u
S : Type v
T : Type w
A : Type z
A' : Type u_1
B' : Type u_2
a b : R
n : ℕ
inst✝² : CommSemiring A'
inst✝¹ : Semiring B'
inst✝ : Ring R
p : R[X]
r : R
bound : natDegree (p * (X - ↑C r)) < natDegree p + 2
| ∑ k in range (natDegree p + 1), coeff (p * (X - ↑C r)) (k + 1) * r ^ (k + 1)
case a
R : Type u
S : Type v
T : Type w
A : Type z
A' : Type u_1
B' : Type u_2
a b : R
n : ℕ
inst✝² : CommSemiring A'
inst✝¹ : Semiring B'
inst✝ : Ring R
p : R[X]
r : R
bound : natDegree (p * (X - ↑C r)) < natDegree p + 2
| coeff (p * (X - ↑C r)) 0 * r ^ 0
[PROOFSTEP]
arg 2
[GOAL]
case a
R : Type u
S : Type v
T : Type w
A : Type z
A' : Type u_1
B' : Type u_2
a b : R
n : ℕ
inst✝² : CommSemiring A'
inst✝¹ : Semiring B'
inst✝ : Ring R
p : R[X]
r : R
bound : natDegree (p * (X - ↑C r)) < natDegree p + 2
| fun k => coeff (p * (X - ↑C r)) (k + 1) * r ^ (k + 1)
case a
R : Type u
S : Type v
T : Type w
A : Type z
A' : Type u_1
B' : Type u_2
a b : R
n : ℕ
inst✝² : CommSemiring A'
inst✝¹ : Semiring B'
inst✝ : Ring R
p : R[X]
r : R
bound : natDegree (p * (X - ↑C r)) < natDegree p + 2
| coeff (p * (X - ↑C r)) 0 * r ^ 0
[PROOFSTEP]
simp [coeff_mul_X_sub_C, sub_mul, mul_assoc, ← pow_succ]
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
A' : Type u_1
B' : Type u_2
a b : R
n : ℕ
inst✝² : CommSemiring A'
inst✝¹ : Semiring B'
inst✝ : Ring R
p : R[X]
r : R
bound : natDegree (p * (X - ↑C r)) < natDegree p + 2
⊢ ∑ k in range (natDegree p + 1), (coeff p k * r ^ (k + 1) - coeff p (k + 1) * r ^ (k + 1 + 1)) +
      coeff (p * (X - ↑C r)) 0 * r ^ 0 =
    0
[PROOFSTEP]
rw [sum_range_sub']
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
A' : Type u_1
B' : Type u_2
a b : R
n : ℕ
inst✝² : CommSemiring A'
inst✝¹ : Semiring B'
inst✝ : Ring R
p : R[X]
r : R
bound : natDegree (p * (X - ↑C r)) < natDegree p + 2
⊢ coeff p 0 * r ^ (0 + 1) - coeff p (natDegree p + 1) * r ^ (natDegree p + 1 + 1) + coeff (p * (X - ↑C r)) 0 * r ^ 0 = 0
[PROOFSTEP]
simp [coeff_monomial]
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
A' : Type u_1
B' : Type u_2
a b : R
n : ℕ
inst✝³ : CommSemiring A'
inst✝² : Semiring B'
inst✝¹ : Ring R
inst✝ : Nontrivial R
r : R
x✝ : IsUnit (X - ↑C r)
g : R[X]
_hfg : (X - ↑C r) * g = 1
hgf : g * (X - ↑C r) = 1
⊢ 0 = 1
[PROOFSTEP]
erw [← eval_mul_X_sub_C, hgf, eval_one]
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
A' : Type u_1
B' : Type u_2
a b : R
n : ℕ
inst✝⁴ : CommSemiring A'
inst✝³ : Semiring B'
M : Type u_3
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : M →ₗ[R] M
v : M
p : R[X]
⊢ ↑(↑(aeval f) p) v = sum p fun n b => b • ↑(f ^ n) v
[PROOFSTEP]
rw [aeval_def, eval₂_eq_sum]
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
A' : Type u_1
B' : Type u_2
a b : R
n : ℕ
inst✝⁴ : CommSemiring A'
inst✝³ : Semiring B'
M : Type u_3
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : M →ₗ[R] M
v : M
p : R[X]
⊢ ↑(sum p fun e a => ↑(algebraMap R (M →ₗ[R] M)) a * f ^ e) v = sum p fun n b => b • ↑(f ^ n) v
[PROOFSTEP]
exact (LinearMap.applyₗ v).map_sum
