Commit 2026-02-02 07:19 7cecd1f8

View on Github →

feat(RingTheory/MvPolynomial): powers of ideal of variables (#33539)

  1. Added a new file Algebra/Group/TypeTags/Pointwise.lean to provide more helper results about pointwise operations on sets
  2. Provided more APIs for MvPolynomial.restrictSupport and defined restrictSupportIdeal to be the ideal determined by restrictSupport R s when s is an upper set
  3. Defined MvPolynomial.idealOfVars to be the ideal spanned by all variables in MvPolynomial and provided results about its powers
  4. Provided some relavent helper results while golfing

Estimated changes

added theorem Set.Ici_mul_Ici_eq
added theorem Set.Ici_one_eq_univ
added theorem Set.Ici_pow_eq
added theorem Finsupp.degree_mono