Commit 2024-03-04 20:11 7f32cc79

View on Github →

chore: split MvPolynomial.Variables (#11094) Splits this file into two. The sections about degree related concepts are totally independent of the vars related concepts so this was a clean split.

Estimated changes

added theorem MvPolynomial.degrees_C
added theorem MvPolynomial.degrees_X
deleted theorem MvPolynomial.degreeOf_C
deleted theorem MvPolynomial.degreeOf_X
deleted theorem MvPolynomial.degreeOf_def
deleted theorem MvPolynomial.degrees_C
deleted theorem MvPolynomial.degrees_X'
deleted theorem MvPolynomial.degrees_X
deleted theorem MvPolynomial.degrees_add
deleted theorem MvPolynomial.degrees_def
deleted theorem MvPolynomial.degrees_map
deleted theorem MvPolynomial.degrees_mul
deleted theorem MvPolynomial.degrees_one
deleted theorem MvPolynomial.degrees_pow
deleted theorem MvPolynomial.degrees_prod
deleted theorem MvPolynomial.degrees_sum
deleted theorem MvPolynomial.degrees_zero
deleted theorem MvPolynomial.mem_degrees