[Merged by Bors] - feat(RingTheory/MvPolynomial/MonomialOrder/Monic): monic polynomials wrt a monomial order#21546
[Merged by Bors] - feat(RingTheory/MvPolynomial/MonomialOrder/Monic): monic polynomials wrt a monomial order#21546AntoineChambert-Loir wants to merge 13 commits intomasterfrom
Conversation
AntoineChambert-Loir
commented
Feb 7, 2025
…wrt a monomial order
PR summary de0d329642
|
| File | Base Count | Head Count | Change |
|---|---|---|---|
| Mathlib.RingTheory.MvPolynomial.MonomialOrder | 1157 | 1158 | +1 (+0.09%) |
Import changes for all files
| Files | Import difference |
|---|---|
3 filesMathlib.RingTheory.MvPolynomial.Groebner Mathlib.RingTheory.MvPolynomial.MonomialOrder.DegLex Mathlib.RingTheory.MvPolynomial.MonomialOrder |
1 |
Declarations diff
+ Monic
+ Monic.add_of_lt
+ Monic.coeff_degree
+ Monic.decidable
+ Monic.leadingCoeff_eq_one
+ Monic.mul
+ Monic.ne_zero
+ Monic.of_subsingleton
+ Monic.pow
+ Monic.prod
+ coeff_pow_nsmul_degree
+ degree_X_add_C
+ degree_X_sub_C
+ degree_mul_of_mul_leadingCoeff_ne_zero
+ degree_one
+ degree_pow
+ degree_pow_le
+ degree_pow_of_pow_leadingCoeff_ne_zero
+ degree_subsingleton
+ leadingCoeff_X
+ leadingCoeff_mul_of_mul_leadingCoeff_ne_zero
+ leadingCoeff_neg
+ leadingCoeff_one
+ leadingCoeff_pow
+ leadingCoeff_pow_of_pow_leadingCoeff_ne_zero
+ monic_X
+ monic_X_add_C
+ monic_X_sub_C
+ monic_monomial
+ monic_monomial_one
+ monic_one
- degree_mul_of_nonzero_mul
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
relativevalue is the weighted sum of the differences with weight given by the inverse of the current value of the statistic. - The
absolutevalue is therelativevalue divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).
Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>
Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>
YaelDillies
left a comment
There was a problem hiding this comment.
Thanks! 🚀
maintainer merge
|
🚀 Pull request has been placed on the maintainer queue by YaelDillies. |
|
Thanks! bors merge |
…wrt a monomial order (#21546)
|
Pull request successfully merged into master. Build succeeded: |
| @[simp] theorem degree_one : m.degree (1 : MvPolynomial σ R) = 0 := by | ||
| obtain h | h' := subsingleton_or_nontrivial R | ||
| · rw [Subsingleton.eq_zero 1, degree_zero] | ||
| · change m.degree (monomial 0 1) = 0 | ||
| classical | ||
| rw [degree_monomial] | ||
| simp |
There was a problem hiding this comment.
(too late) Since you already put degree_subsingleton as @[simp, nontriviality], the first part of the proof could be exact degree_subsingleton or simp, or just replace obtain part by nontriviality R.
There was a problem hiding this comment.
Feel free to open another PR!
There was a problem hiding this comment.