Commit 2024-06-04 21:12 7482cd99

View on Github →

feat(RingTheory/MvPolynomial): add finset of coefficients (#12887) Copies the Polynomial API for the finset of coefficients of a polynomial to the multivariate case.

Estimated changes

Modified Mathlib/Algebra/MvPolynomial/Basic.lean

added theorem MvPolynomial.coeff_mem_coeffs

added def MvPolynomial.coeffs

added theorem MvPolynomial.coeffs_eq_empty_of_subsingleton

added theorem MvPolynomial.coeffs_one

added theorem MvPolynomial.coeffs_one_of_nontrivial

added theorem MvPolynomial.coeffs_zero

added theorem MvPolynomial.mem_coeffs_iff

added theorem MvPolynomial.zero_not_mem_coeffs