feat(FieldTheory/Minpoly): minpoly K x splits implies minpoly K (algebraMap K L a - x) splits

[jjdishere]

Add minpoly K x splits implies minpoly K (- x) splits and minpoly K (algebraMap K L a - x) splits. This is after #17093 .

---

• [x] depends on: #17367
• [ ] depends on: #17093

[github-actions[bot]]

PR summary 8a41b52b74

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

+ Splits.comp_neg_X + Splits.comp_of_degree_le_one + Splits.comp_of_map_degree_le_one + algEquivAevalNegX + algEquivCMulXAddC + algEquivCMulXAddC_symm_eq + comp_neg_X_comp_neg_X + dvd_comp_C_mul_X_add_C_iff + dvd_comp_neg_X_iff + minpoly_algebraMap_sub_splits + minpoly_neg_splits + splits_iff_comp_splits_of_degree_eq_one

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).

[alreadydone]

Doesn't IntermediateField.splits_of_mem_adjoin directly imply the result in the title (and #17903)?

[jjdishere]

Doesn't IntermediateField.splits_of_mem_adjoin directly imply the result in the title (and #17903)?

Thank you very much @alreadydone ! I didn't find this theorem before. For those intermediate results in this PR, I believe they have their own use. For the final results, do you suggest I

1. remove the final results, or
2. keep them and use the IntermediateField.splits_of_mem_adjoin to golf the proof, or
3. keep it as it is?

I think these final lemmas are easier to use than IntermediateField.splits_of_mem_adjoin in other proofs.

[alreadydone]

~~Strangely the diff is still 34 files after you merged master~~ ... (I see, it's because #17403 is not yet merged) I'll take a look at the intermediate results after this is fixed. I think it's good to keep the final results and golf it, but if it requires additional import(s) you may keep your original proof.

[jjdishere]

@alreadydone I've checked the dependency. IntermediateField.splits_of_mem_adjoin live in the file FieldTheory.Normal, which imports FieldTheory.SplittingField.Construction, which imports FieldTheory.SplittingField.IsSplittingField, which imports RingTheory.Adjoin.Field, which is the file my theorems live in.

So indeed it will require additional import(s) (move these lemmas to 3 files later) if I try to use IntermediateField.splits_of_mem_adjoin. What is your opinion on this?

[mathlib4-dependent-issues-bot]

This PR/issue depends on:

• ~~leanprover-community/mathlib4#17367~~
• ~~leanprover-community/mathlib4#17093~~ By Dependent Issues (🤖). Happy coding!

[jcommelin]

maintainer merge

[github-actions[bot]]

🚀 Pull request has been placed on the maintainer queue by jcommelin.

[mathlib-bors[bot]]

:v: jjdishere can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[riccardobrasca]

@jjdishere can you take into account the remaining comments and merge this (ignore the issue about {R} and {R : Type*} for now)? Thanks!

[jjdishere]

bors r+

[mathlib-bors[bot]]

Build failed:

• Build

[riccardobrasca]

Can you please fix the error? Thanks!

[jjdishere]

Can you please fix the error? Thanks!

Sorry for the delay! Fixed.

[jjdishere]

bors r+

[riccardobrasca]

Bors?

bors merge

[mathlib-bors[bot]]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style