Commit 2026-01-03 10:56 758284cc

View on Github →

feat: file for lemmas about MvPolynomials over NoZeroDivisors (#25925) This PR creates a new file for lemmas about MvPolynomials over rings which are NoZeroDivisors, to make modified versions of lemmas like degreeOf_C_mul. Original PR: https://github.com/leanprover-community/mathlib4/pull/11106

  • depends on: #11095
  • depends on: #11094
  • depends on: #25926 [We need this lemma to establish fact about degreeOf n (p + q)]
  • depends on: #32558

Estimated changes