[Merged by Bors] - feat(Algebra/MvPolynomial/Basic): coeff_C_of_ne_zero and coeff_add_single_C#39623

justus-springer wants to merge 13 commits into

leanprover-community:masterleanprover-community/mathlib4:masterfrom

justus-springer:justus/MvPolynomial_coeff_C_lemmasjustus-springer/mathlib4:justus/MvPolynomial_coeff_C_lemmasCopy head branch name to clipboard