Gadget Mul apply

theorem gadgetMul_apply (base : R) {rows digits : Nat} (hd : 0 < digits)    (v : PolyVec (Rq Φ) (rows * digits)) (i : Fin rows) :    gadgetMul Φ base v i      = ∑ e : Fin digits, Rq.constRq Φ (base ^ (e : ℕ)) * v (finProdFinEquiv (i, e)) := by  rw [gadgetMul, matVecMul_apply, dot_eq_sum]  simp only [gadgetMatrix]  rw [← Equiv.sum_comp finProdFinEquiv (fun j => gadgetEntry Φ base i j * v j),      Fintype.sum_prod_type]  rw [Finset.sum_eq_single i]  · apply Finset.sum_congr rfl    intro e _    rw [gadgetEntry_finProdFinEquiv Φ base hd i i e, if_pos rfl]  · intro i' _ hne    apply Finset.sum_eq_zero    intro e _    rw [gadgetEntry_finProdFinEquiv Φ base hd i i' e, if_neg hne, zero_mul]  · intro h    exact absurd (Finset.mem_univ i) h