feat(RingTheory): uniqueness of the lift of a simple root and the adic completeness of artinian local ring#37356
Conversation
github-actions
bot
added
the
large-import
PR summary b301d257a1Import changes exceeding 2%
|
| File | Base Count | Head Count | Change |
|---|---|---|---|
| Mathlib.RingTheory.AdicCompletion.Noetherian | 1369 | 1835 | +466 (+34.04%) |
Import changes for all files
| Files | Import difference |
|---|---|
Mathlib.RingTheory.AdicCompletion.Noetherian |
466 |
Declarations diff
+ IsLocalRing.eq_of_eval_eq_zero_of_not_isUnit_sub
+ exists_mul_sq_add_linear_part_eq_eval_add
+ instance (priority := 100) {A : Type*} [CommRing A] [IsArtinianRing A] [IsLocalRing A] :
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).
|
could you indicate what you are adding in the PR title? |
BryceT233
changed the title
|
The lemmas felt a bit disjointed, and I couldn't think of a good way to summarize them without making the title overly long, so I took the easy way out. I've updated it to better reflect the contents |
|
if they're independent, then you can make 2 smaller PRs (I know it's annoying) |
2 participants
This PR adds the following three lemmas:
Polynomial.exists_mul_sq_add_linear_part_eq_eval_add: this is an alternative version ofPolynomial.eval_add_of_sq_eq_zeroand is used in the lemmaIsLocalRing.eq_of_eval_eq_zero_of_not_isUnit_sub.IsLocalRing.eq_of_eval_eq_zero_of_not_isUnit_sub: this is stacks [06RR] which shows the uniqueness of the lift of a simple root given by the henselian property.