(col : ℕ → (ℕ →₀ ℂ)) (k : ℕ) : dGamma col (Finsupp.single (Finsupp.single k 1) 1) = ∑ j ∈ (col k).support, (col k) j • Finsupp.single (Finsupp.single j 1) (1 : ℂ)

Initializing...

(col : ℕ → (ℕ →₀ ℂ)) (k : ℕ) : dGamma col (Finsupp.single (Finsupp.single k 1) 1) = ∑ j ∈ (col k).support, (col k) j • Finsupp.single (Finsupp.single j 1) (1 : ℂ) · Prove2Me