feat(Adjoin/Polynomial): Split file and add RingHom/Transcendental lemmas

[xgenereux]

This PR adds 3 maps, some of them requiring that the element x is transcendental over R:

• equivRangeAevalAdjoinSingleton : (aeval (R := R) x).range ≃ₐ[R] adjoin R {x}
• equivPolynomialRangeAEval : R[X] ≃ₐ[R] (aeval (R := R) x).range
• equivPolynomialAdjoin : R[X] ≃ₐ[R] Algebra.adjoin R {x}

I created a new folder because the lemmas are related to Polynomial and adjoining elements, but can't be in the same file as Transcendental depends on Adjoin/Polynomial.lean.

I have also reorganized the file.

Co-authored-by: María Inés de Frutos Fernández <mariaines.dff@gmail.com>

---

• depends on: chore(Adjoin/Polynomial): Move file Adjoin/Polynomial to Adjoin/Polynomial/Basic to allow for future changes #35883

[github-actions]

PR summary a5a17ebb89

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.RingTheory.Adjoin.Polynomial	1129	0	-1129 (-100.00%)

Import changes for all files

Files	Import difference
Mathlib.RingTheory.Adjoin.Polynomial	-1129
Mathlib.RingTheory.Adjoin.Polynomial.Basic (new file)	1129
Mathlib.RingTheory.Adjoin.Polynomial.Transcendental (new file)	1382

---

Declarations diff

+ _root_.Polynomial.adjoin_X
+ _root_.Polynomial.aeval_mem_adjoin_singleton
+ adjoin_eq_exists_aeval
+ adjoin_mem_exists_aeval
+ adjoin_singleton_eq_range_aeval
+ adjoin_singleton_induction
+ equivPolynomialAdjoin
+ equivPolynomialAdjoin_apply_X
+ equivPolynomialAdjoin_coe_eq
+ equivPolynomialAdjoin_def
+ equivPolynomialRangeAEval
+ equivPolynomialRangeAEval_coe_eq
+ equivPolynomialRangeAEval_def
+ equivRangeAevalAdjoinSingleton
+ equivRangeAevalAdjoinSingleton_apply
+ equivRangeAevalAdjoinSingleton_apply'
- _root_.Algebra.adjoin_eq_exists_aeval
- _root_.Algebra.adjoin_mem_exists_aeval
- _root_.Algebra.adjoin_singleton_eq_range_aeval
- _root_.Algebra.adjoin_singleton_induction
- adjoin_X
- aeval_mem_adjoin_singleton

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

---

note: file Mathlib/RingTheory/Adjoin/Polynomial.lean was removed.
Please create a follow-up pull request adding a module deprecation. Thanks!

[grunweg]

Can you split the file rename into its own PR? That will make this PR easier to review (and I'll be happy to approve the rename). Thanks!

[xgenereux]

You want me to make a PR that is a simply the rename of Mathlib.RingTheory.Adjoin.Polynomial to Mathlib.RingTheory.Adjoin.Polynomial.Basic?

Can you help me understand why such a simple change needs it's own PR?
Thanks!

[joneugster]

t-algebra

[xgenereux]

Anyways I've split the first commit. The PR #35883 contains the split and a few minor changes (I hope that's fine).

[mathlib-dependent-issues]

This PR/issue depends on:

• chore(Adjoin/Polynomial): Move file Adjoin/Polynomial to Adjoin/Polynomial/Basic to allow for future changes #35883
  By Dependent Issues (🤖). Happy coding!