∀ {R : Type u_1} {σ : Type u_2} {n : σ} [inst : CommSemiring R] [NoZeroDivisors R] {ι : Type u_3} (s : Finset ι)
  (f : ι → MvPolynomial σ R),
  (∀ i ∈ s, f i ≠ 0) → MvPolynomial.degreeOf n (∏ i ∈ s, f i) = ∑ i ∈ s, MvPolynomial.degreeOf n (f i)