R : Type u
S : Type v
T : Type w
A : Type z
A' : Type ?u.893198
B' : Type ?u.893201
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_2
inst✝² : Semiring B
inst✝¹ : Algebra R B
x✝ : A
F : Type u_1
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))
R : Type u
S : Type v
T : Type w
A : Type z
A' : Type ?u.893198
B' : Type ?u.893201
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_2
inst✝² : Semiring B
inst✝¹ : Algebra R B
x✝ : A
F : Type u_1
inst✝ : AlgHomClass F R A B
f : F
x : A
p : R[X]
⊢ ↑(aeval (↑f x)) p = ↑f (↑(aeval x) p)
refine' Polynomial.induction_on p (by simp [AlgHomClass.commutes]) (fun p q hp hq => _)
  (by simp [AlgHomClass.commutes])
no goals
R : Type u
S : Type v
T : Type w
A : Type z
A' : Type ?u.893198
B' : Type ?u.893201
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_2
inst✝² : Semiring B
inst✝¹ : Algebra R B
x✝ : A
F : Type u_1
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))
rw [map_add, hp, hq, ← map_add, ← map_add]
no goals
R : Type u
S : Type v
T : Type w
A : Type z
A' : Type ?u.893198
B' : Type ?u.893201
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_2
inst✝² : Semiring B
inst✝¹ : Algebra R B
x✝ : A
F : Type u_1
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))
simp [AlgHomClass.commutes]
no goals
R : Type u
S : Type v
T : Type w
A : Type z
A' : Type ?u.893198
B' : Type ?u.893201
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_2
inst✝² : Semiring B
inst✝¹ : Algebra R B
x✝ : A
F : Type u_1
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)))
simp [AlgHomClass.commutes]