(e : ℕ → ℝ) (k : ℕ) : dGamma (diagCol e) (Finsupp.single (Finsupp.single k 1) (1 : ℂ)) = ((e k : ℝ) : ℂ) • Finsupp.single (Finsupp.single k 1) (1 : ℂ)

Initializing...

(e : ℕ → ℝ) (k : ℕ) : dGamma (diagCol e) (Finsupp.single (Finsupp.single k 1) (1 : ℂ)) = ((e k : ℝ) : ℂ) • Finsupp.single (Finsupp.single k 1) (1 : ℂ) · Prove2Me