Commit 2022-01-11 11:13 ebbc973b

View on Github →

feat(data/mv_polynomial): assorted mv_polynomial and finsupp lemmas (#11319) Mostly around total degree, supports and homogeneous components. From flt-regular.

Estimated changes

Modified src/data/finsupp/basic.lean

added theorem finsupp.support_smul_eq

Modified src/data/mv_polynomial/basic.lean

added theorem mv_polynomial.monomial_eq_zero

modified theorem mv_polynomial.monomial_zero

Modified src/data/mv_polynomial/variables.lean

added theorem mv_polynomial.total_degree_X_pow

added theorem mv_polynomial.total_degree_monomial

Modified src/ring_theory/polynomial/homogeneous.lean

added theorem mv_polynomial.homogeneous_component_C_mul

added theorem mv_polynomial.is_homogeneous_of_total_degree_zero