∀ {S₁ : Type v} {σ : Type u_1} [inst : CommSemiring S₁] {R : Type u_2} [inst_1 : SMulZeroClass R S₁] (a : R)
  (f : MvPolynomial σ S₁), MvPolynomial.constantCoeff (a • f) = a • MvPolynomial.constantCoeff f