Theorem MvPolynomial.coeffs_one_of_nontrivial

Modification history

2024-06-04 21:12
Mathlib/Algebra/MvPolynomial/Basic.lean
feat(RingTheory/MvPolynomial): add finset of coefficients (#12887) …
Added MvPolynomial.coeffs_one_of_nontrivialView on Github →