R : Type u
S : Type v
T : Type w
A : Type z
A' : Type ?u.1305085
B' : Type ?u.1305088
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.1305301
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
R : Type u
S : Type v
T : Type w
A : Type z
A' : Type ?u.1305085
B' : Type ?u.1305088
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.1305301
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
intro h
case a
R : Type u
S : Type v
T : Type w
A : Type z
A' : Type ?u.1305085
B' : Type ?u.1305088
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.1305301
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
R : Type u
S : Type v
T : Type w
A : Type z
A' : Type ?u.1305085
B' : Type ?u.1305088
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.1305301
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
apply hf
no goals
case a
R : Type u
S : Type v
T : Type w
A : Type z
A' : Type ?u.1305085
B' : Type ?u.1305088
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.1305301
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
rw [← eval₂_hom, h, f.map_zero]