Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-09-28 20:09 e2cb9e19

View on Github →

feat(data/mv_polynomial/supported): subalgebra of polynomials supported by a set of variables (#9183)

Estimated changes

Modified src/algebra/algebra/basic.lean

added theorem alg_equiv.symm_trans_apply

Created src/data/mv_polynomial/supported.lean

added theorem mv_polynomial.X_mem_supported

added theorem mv_polynomial.mem_supported

added theorem mv_polynomial.mem_supported_vars

added theorem mv_polynomial.supported_empty

added theorem mv_polynomial.supported_eq_adjoin_X

added theorem mv_polynomial.supported_eq_range_rename

added theorem mv_polynomial.supported_eq_vars_subset

added theorem mv_polynomial.supported_equiv_mv_polynomial_symm_C

added theorem mv_polynomial.supported_equiv_mv_polynomial_symm_X

added theorem mv_polynomial.supported_le_supported_iff

added theorem mv_polynomial.supported_mono

added theorem mv_polynomial.supported_strict_mono

added theorem mv_polynomial.supported_univ

Modified src/data/mv_polynomial/variables.lean

added theorem mv_polynomial.exists_rename_eq_of_vars_subset_range

added theorem mv_polynomial.hom_congr_vars