`BookProof.ChapterF1.bargmann_eq_sum` (p q : ℂ[X]) {s : Finset ℕ} (hp : p.support ⊆ s) (hq : q.support ⊆ s) : bargmann p q = ∑ n ∈ s, (n.factorial : ℂ) * (starRingEnd ℂ) (p.coeff n

Initializing...

`BookProof.ChapterF1.bargmann_eq_sum` (p q : ℂ[X]) {s : Finset ℕ} (hp : p.support ⊆ s) (hq : q.support ⊆ s) : bargmann p q = ∑ n ∈ s, (n.factorial : ℂ) * (starRingEnd ℂ) (p.coeff n · Prove2Me