{m : ℕ} (w : Fin m → E) (c : EuclideanSpace ℂ (Fin m)) (x : E) : ⟪synthesis w c, x⟫_ℂ = ∑ i, (starRingEnd ℂ) (c i) * ⟪w i, x⟫_ℂ

Initializing...

{m : ℕ} (w : Fin m → E) (c : EuclideanSpace ℂ (Fin m)) (x : E) : ⟪synthesis w c, x⟫_ℂ = ∑ i, (starRingEnd ℂ) (c i) * ⟪w i, x⟫_ℂ · Prove2Me