R : Type u_2
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : Infinite R
σ : Type u_1
p : MvPolynomial σ R
⊢ ∀ (x : σ → R), ↑(eval x) p = ↑(eval x) p
R : Type u_2
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : Infinite R
σ : Type u_1
p q : MvPolynomial σ R
⊢ p = q → ∀ (x : σ → R), ↑(eval x) p = ↑(eval x) q
rintro rfl
no goals
R : Type u_2
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : Infinite R
σ : Type u_1
p : MvPolynomial σ R
⊢ ∀ (x : σ → R), ↑(eval x) p = ↑(eval x) p
simp only [forall_const, eq_self_iff_true]