Commit 2025-05-26 14:12 696e851a

View on Github →

feat(Algebra/MvPolynomial): add MvPolynomial.mem_range_map_of_coeffs_subset (#24785)

Estimated changes

Modified Mathlib/Algebra/MvPolynomial/Basic.lean

added theorem MvPolynomial.coeffs_C

added theorem MvPolynomial.coeffs_C_subset

added theorem MvPolynomial.coeffs_X_mul

added theorem MvPolynomial.coeffs_add

added theorem MvPolynomial.coeffs_mul_X

added theorem MvPolynomial.disjoint_support_monomial

added theorem MvPolynomial.mem_coeffsIn_iff_coeffs_subset

Modified Mathlib/Algebra/MvPolynomial/Eval.lean

added theorem MvPolynomial.coe_coeffs_map

added theorem MvPolynomial.coeffs_map

added theorem MvPolynomial.mem_range_map_iff_coeffs_subset

added theorem MvPolynomial.range_mapAlgHom