R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
f g : R[X]
s : Finset R
degree_f_lt : f ∈ degreeLT R (Finset.card s)
eval_f : ∀ (x : R), x ∈ s → eval x f = 0
⊢ f = 0
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
f g : R[X]
s : Finset R
degree_f_lt : degree f < ↑(Finset.card s)
eval_f : ∀ (x : R), x ∈ s → eval x f = 0
⊢ f = 0
rw [← mem_degreeLT] at degree_f_lt
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
f g : R[X]
s : Finset R
degree_f_lt : f ∈ degreeLT R (Finset.card s)
eval_f :
  ∀ (x : R),
    x ∈ s →
      ∑ x_1 : Fin (Finset.card s),
          ↑(degreeLTEquiv R (Finset.card s)) { val := f, property := degree_f_lt } x_1 * x ^ ↑x_1 =
        0
⊢ f = 0
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
f g : R[X]
s : Finset R
degree_f_lt : f ∈ degreeLT R (Finset.card s)
eval_f : ∀ (x : R), x ∈ s → eval x f = 0
⊢ f = 0
simp_rw [eval_eq_sum_degreeLTEquiv degree_f_lt] at eval_f
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
f g : R[X]
s : Finset R
degree_f_lt : f ∈ degreeLT R (Finset.card s)
eval_f :
  ∀ (x : R),
    x ∈ s →
      ∑ x_1 : Fin (Finset.card s),
          ↑(degreeLTEquiv R (Finset.card s)) { val := f, property := degree_f_lt } x_1 * x ^ ↑x_1 =
        0
⊢ ↑(degreeLTEquiv R (Finset.card s)) { val := f, property := degree_f_lt } = 0
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
f g : R[X]
s : Finset R
degree_f_lt : f ∈ degreeLT R (Finset.card s)
eval_f :
  ∀ (x : R),
    x ∈ s →
      ∑ x_1 : Fin (Finset.card s),
          ↑(degreeLTEquiv R (Finset.card s)) { val := f, property := degree_f_lt } x_1 * x ^ ↑x_1 =
        0
⊢ f = 0
rw [← degreeLTEquiv_eq_zero_iff_eq_zero degree_f_lt]
no goals
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
f g : R[X]
s : Finset R
degree_f_lt : f ∈ degreeLT R (Finset.card s)
eval_f :
  ∀ (x : R),
    x ∈ s →
      ∑ x_1 : Fin (Finset.card s),
          ↑(degreeLTEquiv R (Finset.card s)) { val := f, property := degree_f_lt } x_1 * x ^ ↑x_1 =
        0
⊢ ↑(degreeLTEquiv R (Finset.card s)) { val := f, property := degree_f_lt } = 0
exact
  Matrix.eq_zero_of_forall_index_sum_mul_pow_eq_zero
    (Injective.comp (Embedding.subtype _).inj' (equivFinOfCardEq (card_coe _)).symm.injective)
    fun _ => eval_f _ (Finset.coe_mem _)