𝕜 : Type u_1
E : Type ?u.296852
F : Type ?u.296855
β : Type ?u.296858
ι : Type u_2
inst✝¹ : OrderedSemiring 𝕜
inst✝ : Fintype ι
i j : ι
⊢ 0 ≤ if i = j then 1 else 0
𝕜 : Type u_1
E : Type ?u.296852
F : Type ?u.296855
β : Type ?u.296858
ι : Type u_2
inst✝¹ : OrderedSemiring 𝕜
inst✝ : Fintype ι
i j : ι
⊢ 0 ≤ (fun j => if i = j then 1 else 0) j
simp only
no goals
𝕜 : Type u_1
E : Type ?u.296852
F : Type ?u.296855
β : Type ?u.296858
ι : Type u_2
inst✝¹ : OrderedSemiring 𝕜
inst✝ : Fintype ι
i j : ι
⊢ 0 ≤ if i = j then 1 else 0
split_ifs <;> norm_num
no goals
𝕜 : Type u_1
E : Type ?u.296852
F : Type ?u.296855
β : Type ?u.296858
ι : Type u_2
inst✝¹ : OrderedSemiring 𝕜
inst✝ : Fintype ι
i : ι
⊢ ∑ x : ι, (fun j => if i = j then 1 else 0) x = 1
rw [Finset.sum_ite_eq, if_pos (Finset.mem_univ _)]