R : Type u
S : Type v
T : Type w
a b : R
n : ℕ
inst✝¹ : CommRing R
inst✝ : IsDomain R
p✝ q✝ p q : R[X]
h : Set.Infinite {x | eval x p = eval x q}
⊢ p - q = 0
R : Type u
S : Type v
T : Type w
a b : R
n : ℕ
inst✝¹ : CommRing R
inst✝ : IsDomain R
p✝ q✝ p q : R[X]
h : Set.Infinite {x | eval x p = eval x q}
⊢ p = q
rw [← sub_eq_zero]
case h
R : Type u
S : Type v
T : Type w
a b : R
n : ℕ
inst✝¹ : CommRing R
inst✝ : IsDomain R
p✝ q✝ p q : R[X]
h : Set.Infinite {x | eval x p = eval x q}
⊢ Set.Infinite {x | IsRoot (p - q) x}
R : Type u
S : Type v
T : Type w
a b : R
n : ℕ
inst✝¹ : CommRing R
inst✝ : IsDomain R
p✝ q✝ p q : R[X]
h : Set.Infinite {x | eval x p = eval x q}
⊢ p - q = 0
apply eq_zero_of_infinite_isRoot
no goals
case h
R : Type u
S : Type v
T : Type w
a b : R
n : ℕ
inst✝¹ : CommRing R
inst✝ : IsDomain R
p✝ q✝ p q : R[X]
h : Set.Infinite {x | eval x p = eval x q}
⊢ Set.Infinite {x | IsRoot (p - q) x}
simpa only [IsRoot, eval_sub, sub_eq_zero]