K : Type u_1
σ : Type u_2
inst✝² : Fintype K
inst✝¹ : Fintype σ
inst✝ : CommRing K
a : σ → K
✝ : Nontrivial ((fun x => K) (indicator a))
⊢ ↑(eval a) (indicator a) = 1
K : Type u_1
σ : Type u_2
inst✝² : Fintype K
inst✝¹ : Fintype σ
inst✝ : CommRing K
a : σ → K
⊢ ↑(eval a) (indicator a) = 1
nontriviality
K : Type u_1
σ : Type u_2
inst✝² : Fintype K
inst✝¹ : Fintype σ
inst✝ : CommRing K
a : σ → K
✝ : Nontrivial ((fun x => K) (indicator a))
this : 0 < Fintype.card K - 1
⊢ ↑(eval a) (indicator a) = 1
K : Type u_1
σ : Type u_2
inst✝² : Fintype K
inst✝¹ : Fintype σ
inst✝ : CommRing K
a : σ → K
✝ : Nontrivial ((fun x => K) (indicator a))
⊢ ↑(eval a) (indicator a) = 1
have : 0 < Fintype.card K - 1 := tsub_pos_of_lt Fintype.one_lt_card
no goals
K : Type u_1
σ : Type u_2
inst✝² : Fintype K
inst✝¹ : Fintype σ
inst✝ : CommRing K
a : σ → K
✝ : Nontrivial ((fun x => K) (indicator a))
this : 0 < Fintype.card K - 1
⊢ ↑(eval a) (indicator a) = 1
simp only [indicator, map_prod, map_sub, map_one, map_pow, eval_X, eval_C, sub_self,
  zero_pow this, sub_zero, Finset.prod_const_one]