Commit 2025-03-14 09:41 561c554d

View on Github →

chore: rename induction_on''' (#22848) This PR addresses a few things:

  • It renames MvPolynomial.induction_on''' (three primes!) to MvPolynomial.monomial_add_induction_on, addressing a particularly egregious instance of the docPrime linter.
  • It improves the docstrings of this and nearby induction principles to be a bit more clear.
  • It changes the type of a component of the argument of some of these from (σ →₀ ℕ) →₀ R to MvPolynomial σ R, making the theorems more readable and addressing two porting notes.

Estimated changes

modified theorem MvPolynomial.induction_on''
modified theorem MvPolynomial.induction_on