Commit 2025-04-29 10:02 3f255637

View on Github →

feat(Algebra/MvPolynomial): total degrees of some constructions (#24346)

Estimated changes

Modified Mathlib/Algebra/MvPolynomial/Degrees.lean

added theorem MvPolynomial.totalDegree_renameEquiv

Modified Mathlib/Algebra/MvPolynomial/Equiv.lean

added theorem MvPolynomial.natDegree_optionEquivLeft

added theorem MvPolynomial.totalDegree_coeff_optionEquivLeft_add_le

added theorem MvPolynomial.totalDegree_coeff_optionEquivLeft_le

Modified Mathlib/Data/Finsupp/Basic.lean

added theorem Finsupp.embDomain_some_none

added theorem Finsupp.some_embDomain_some

Modified Mathlib/RingTheory/Algebraic/MvPolynomial.lean