feat(RingTheory/MvPolynomial/MonomialOrder): add degree with ⊥ as degree of 0#34759
feat(RingTheory/MvPolynomial/MonomialOrder): add degree with ⊥ as degree of 0#34759Hagb wants to merge 25 commits intoleanprover-community:masterfrom
⊥ as degree of 0#34759Conversation
PR summary d7385d0300
|
| File | Base Count | Head Count | Change |
|---|---|---|---|
| Mathlib.Data.Finsupp.MonomialOrder | 823 | 824 | +1 (+0.12%) |
Import changes for all files
| Files | Import difference |
|---|---|
Mathlib.Data.Finsupp.MonomialOrder |
1 |
Declarations diff
+ bot_lt_toWithBotSyn_apply_iff
+ degree_eq_unbotD_withBotDegree
+ le_withBotDegree
+ toWithBotSyn
+ toWithBotSyn_apply
+ toWithBotSyn_apply_bot
+ toWithBotSyn_apply_coe
+ toWithBotSyn_apply_eq_bot_iff
+ toWithBotSyn_apply_le_bot_iff
+ toWithBotSyn_symm_apply_bot
+ toWithBotSyn_symm_apply_eq_bot
+ toWithBotSyn_withBotDegree_mul_le
+ withBotDegree
+ withBotDegree_C
+ withBotDegree_add_le
+ withBotDegree_add_of_lt
+ withBotDegree_add_of_right_lt
+ withBotDegree_eq
+ withBotDegree_eq_bot_iff
+ withBotDegree_eq_coe_degree_iff
+ withBotDegree_eq_withBotDegree_iff
+ withBotDegree_le_withBotDegree_iff
+ withBotDegree_le_withBotDegree_iff_of_ne_zero
+ withBotDegree_le_withBotDegree_of_support_subset
+ withBotDegree_leadingTerm
+ withBotDegree_lt_withBotDegree_iff
+ withBotDegree_lt_withBotDegree_iff_of_ne_zero
+ withBotDegree_monomial
+ withBotDegree_mul
+ withBotDegree_mul_le
+ withBotDegree_mul_of_left_mem_nonZeroDivisors
+ withBotDegree_mul_of_right_mem_nonZeroDivisors
+ withBotDegree_neg
+ withBotDegree_one
+ withBotDegree_sum_le
+ withBotDegree_zero
You can run this locally as follows
## summary with just the declaration names:
./scripts/pr_summary/declarations_diff.sh <optional_commit>
## more verbose report:
./scripts/pr_summary/declarations_diff.sh long <optional_commit>The doc-module for scripts/pr_summary/declarations_diff.sh contains some details about this script.
No changes to technical debt.
You can run this locally as
./scripts/reporting/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).
✅ PR Title Formatted CorrectlyThe title of this PR has been updated to match our commit style conventions. |
Hagb
changed the title
⊥ as degree of 0
Hagb
changed the title
⊥ as degree of 0⊥ as degree of 0
Hagb
changed the title
⊥ as degree of 0⊥ as degree of 0
Hagb
changed the title
⊥ as degree of 0 ⊥ as degree of 0
mathlib-dependent-issues
bot
added
the
blocked-by-other-PR
…e with ⊥ as degree of 0
|
you can now comment on the PR to add missing topic labels: t-ring-theory (improvements to the automation are on the way: #34078) |
Co-authored-by: Andrew Yang <[email protected]>
Co-authored-by: Andrew Yang <[email protected]>
Co-authored-by: Andrew Yang <[email protected]>
|
This pull request has conflicts, please merge |
mathlib-merge-conflicts
bot
added
the
merge-conflict
mathlib-dependent-issues
bot
removed
the
blocked-by-other-PR
…hBot` (leanprover-community#34756) It is like `Equiv.withBotCongr` but preserving also addition (`AddEquiv`), for a variant of degree of `MvPolynomial` that maps `0` to `⊥` submitted in leanprover-community#34759.
github-actions
bot
removed
the
merge-conflict
|
This PR/issue depends on: |
…hBot` (leanprover-community#34756) It is like `Equiv.withBotCongr` but preserving also addition (`AddEquiv`), for a variant of degree of `MvPolynomial` that maps `0` to `⊥` submitted in leanprover-community#34759.
2 participants
withBotDegreeis to distinguish the degree of zero polynomial from the degree of non-zero constant polynomial.MonomialOrder.degreeof both are 0, whilewithBotDegreeis⊥for zero polynomial and 0 for non-zero constant polynomial.MonomialOrder.withBotDegreeis toMonomialOrder.degreeasPolynomial.degreeis toPolynomial.natDegree.It's upstreamized from https://github.com/WuProver/groebner_proj.
It's upstream from
Groebner/MonomialOrder.leanin the repoWuProver/groebner_proj.depends on: feat(Logic/Basic):a ∧ (a → b) ↔ a ∧ band(a → b) ∧ a ↔ b ∧ a#34755AddEquivbetweenWithBot#34756