R : Type u
S : Type v
K : Type w
inst✝ : CommRing R
f p : R[X]
x : R
⊢ ↑(algebraMap R (AdjoinRoot f)) x = ↑(mk f) (↑C x)
R : Type u
S : Type v
K : Type w
inst✝ : CommRing R
f p : R[X]
x : R
⊢ ↑(aeval (root f)) (↑C x) = ↑(mk f) (↑C x)
rw [aeval_C]
no goals
R : Type u
S : Type v
K : Type w
inst✝ : CommRing R
f p : R[X]
x : R
⊢ ↑(algebraMap R (AdjoinRoot f)) x = ↑(mk f) (↑C x)
rfl
no goals
R : Type u
S : Type v
K : Type w
inst✝ : CommRing R
f p✝ p q : R[X]
ihp : ↑(aeval (root f)) p = ↑(mk f) p
ihq : ↑(aeval (root f)) q = ↑(mk f) q
⊢ ↑(aeval (root f)) (p + q) = ↑(mk f) (p + q)
rw [AlgHom.map_add, RingHom.map_add, ihp, ihq]
R : Type u
S : Type v
K : Type w
inst✝ : CommRing R
f p : R[X]
n : ℕ
x : R
x✝ : ↑(aeval (root f)) (↑C x * X ^ n) = ↑(mk f) (↑C x * X ^ n)
⊢ ↑(algebraMap R (AdjoinRoot f)) x * root f ^ (n + 1) = ↑(of f) x * root f ^ (n + 1)
R : Type u
S : Type v
K : Type w
inst✝ : CommRing R
f p : R[X]
n : ℕ
x : R
x✝ : ↑(aeval (root f)) (↑C x * X ^ n) = ↑(mk f) (↑C x * X ^ n)
⊢ ↑(aeval (root f)) (↑C x * X ^ (n + 1)) = ↑(mk f) (↑C x * X ^ (n + 1))
rw [AlgHom.map_mul, aeval_C, AlgHom.map_pow, aeval_X, RingHom.map_mul, mk_C, RingHom.map_pow,
  mk_X]
no goals
R : Type u
S : Type v
K : Type w
inst✝ : CommRing R
f p : R[X]
n : ℕ
x : R
x✝ : ↑(aeval (root f)) (↑C x * X ^ n) = ↑(mk f) (↑C x * X ^ n)
⊢ ↑(algebraMap R (AdjoinRoot f)) x * root f ^ (n + 1) = ↑(of f) x * root f ^ (n + 1)
rfl