Commit 2023-03-18 14:58 2453c08c

View on Github →

feat: port Data.MvPolynomial.Supported (#2972)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/MvPolynomial/Supported.lean

added theorem MvPolynomial.X_mem_supported

added theorem MvPolynomial.exists_restrict_to_vars

added theorem MvPolynomial.mem_supported

added theorem MvPolynomial.mem_supported_vars

added theorem MvPolynomial.supportedEquivMvPolynomial_symm_C

added theorem MvPolynomial.supportedEquivMvPolynomial_symm_X

added theorem MvPolynomial.supported_empty

added theorem MvPolynomial.supported_eq_adjoin_X

added theorem MvPolynomial.supported_eq_range_rename

added theorem MvPolynomial.supported_eq_vars_subset

added theorem MvPolynomial.supported_le_supported_iff

added theorem MvPolynomial.supported_mono

added theorem MvPolynomial.supported_strictMono

added theorem MvPolynomial.supported_univ