[Merged by Bors] - feat: file for lemmas about MvPolynomials over NoZeroDivisors

[BoltonBailey]

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: #11106

• depends on: [Merged by Bors] - feat: Option {b // b ≠ a} ≃ α #11095
• depends on: [Merged by Bors] - chore: split MvPolynomial.Variables #11094
• depends on: [Merged by Bors] - feat(Algebra/MvPolynomial/Equiv): degreeOf_eq_natDegree #25926 [We need this lemma to establish fact about degreeOf n (p + q)]
• depends on: [Merged by Bors] - chore(RingTheory/MvPolynomial): weaken IsCancelMulZero to NoZeroDivisors in degree_mul and related lemmas. #32558

---

Notes to self:

• Can the results in this file be generalized?
• Perhaps to the assumption IsCancelMulZero R?
  • Note that when R is a ring, IsCancelMulZero R is equivalent to
    NoZeroDivisors R.
  • When R is only a semiring, NoZeroDivisors R is implied by IsCancelMulZero R
    (although this is not typeclass inferrable, see IsLeftCancelMulZero.to_noZeroDivisors),
  • When R is only a semiring, IsCancelMulZero R is not implied by NoZeroDivisors R, see https://leanprover.zulipchat.com/#narrow/channel/116395-maths/topic/IsCancelMulZero.20and.20NoZeroDivisors.20for.20semirings/with/562333254
  • Thus, we should see if the results in this file can be generalized to
    IsCancelMulZero R.
  • Note that MvPolynomial.totalDegree_mul_of_isDomain exists, which proves a related result
    under the assumption IsCancelMulZero R.
  • This seems weaker than it could be!
  • I will try to open PR to generalize these results to NoZeroDivisors R in a new PR.
• Perhaps to more specific assumptions about cancellation on leadingCoeffs?

This PR continues the work from #11106 and #11073

[github-actions]

PR summary 519f4546a1

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
Mathlib.FieldTheory.SeparablyGenerated Mathlib.RingTheory.MvPolynomial.IrreducibleQuadratic	1
Mathlib.Algebra.MvPolynomial.NoZeroDivisors (new file)	1028

---

Declarations diff

+ degreeOf_C_mul
+ degreeOf_mul_eq
+ degreeOf_one
+ degreeOf_pow_eq
+ degreeOf_prod_eq
+ degrees_mul_eq

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

---

No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[riccardobrasca]

I think we can live with aesop instead of grind at the moment, so this LGTM, thanks!

bors merge

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Lint style
• Post-Build Step
• Build