chore(RingTheory/Adjoin/Polynomial): move to Basic.lean (#35883)

Future changes in #35864 will add a new file `Transcendental.lean`.

Co-authored-by: Xavier Genereux <xaviergenereux@hotmail.com>

Author: xgenereux

Mathlib.lean

@@ -6024,7 +6024,7 @@ public import Mathlib.RingTheory.Adjoin.Dimension
 public import Mathlib.RingTheory.Adjoin.FG
 public import Mathlib.RingTheory.Adjoin.FGBaseChange
 public import Mathlib.RingTheory.Adjoin.Field
-public import Mathlib.RingTheory.Adjoin.Polynomial
+public import Mathlib.RingTheory.Adjoin.Polynomial.Basic
 public import Mathlib.RingTheory.Adjoin.PowerBasis
 public import Mathlib.RingTheory.Adjoin.Singleton
 public import Mathlib.RingTheory.Adjoin.Tower

Mathlib/Algebra/Polynomial/Derivation.lean

@@ -8,7 +8,7 @@ module
 public import Mathlib.Algebra.Polynomial.AlgebraMap
 public import Mathlib.Algebra.Polynomial.Derivative
 public import Mathlib.Algebra.Polynomial.Module.AEval
-public import Mathlib.RingTheory.Adjoin.Polynomial
+public import Mathlib.RingTheory.Adjoin.Polynomial.Basic
 public import Mathlib.RingTheory.Derivation.Basic
 /-!
 # Derivations of univariate polynomials

Mathlib/RingTheory/Adjoin/Polynomial.lean …/RingTheory/Adjoin/Polynomial/Basic.leanMathlib/RingTheory/Adjoin/Polynomial.lean renamed to Mathlib/RingTheory/Adjoin/Polynomial/Basic.lean Mathlib/RingTheory/Adjoin/Polynomial.lean renamed to Mathlib/RingTheory/Adjoin/Polynomial/Basic.lean

@@ -12,8 +12,11 @@ public import Mathlib.Algebra.Polynomial.AlgebraMap
 
 ## Main results
 
-* `Polynomial.instCommSemiringAdjoinSingleton, instCommRingAdjoinSingleton`:
+* `Algebra.instCommSemiringAdjoinSingleton, Algebra.instCommRingAdjoinSingleton`:
   adjoining an element to a commutative (semi)ring gives a commutative (semi)ring
+* `Algebra.adjoin_singleton_induction`:
+  proving a fact about `a : adjoin R {x}` is the same as proving it for `aeval x p` where `p`
+  is an arbitrary polynomial
 -/
 
 @[expose] public section
@@ -24,7 +27,7 @@ open Finset
 
 open Polynomial
 
-namespace Polynomial
+namespace Algebra
 
 universe u v w z
 
@@ -39,53 +42,55 @@ variable [Algebra R A] [Algebra R B]
 variable {p q : R[X]} (x : A)
 
 @[simp]
-theorem adjoin_X : adjoin R ({X} : Set R[X]) = ⊤ := by
+theorem _root_.Polynomial.adjoin_X : adjoin R ({X} : Set R[X]) = ⊤ := by
   refine top_unique fun p _hp => ?_
   set S := adjoin R ({X} : Set R[X])
   rw [← sum_monomial_eq p]; simp only [← smul_X_eq_monomial]
   exact S.sum_mem fun n _hn => S.smul_mem (S.pow_mem (subset_adjoin rfl) _) _
 
 variable (R)
-theorem _root_.Algebra.adjoin_singleton_eq_range_aeval (x : A) :
+theorem adjoin_singleton_eq_range_aeval (x : A) :
     adjoin R {x} = (aeval x).range := by
   rw [← Algebra.map_top, ← adjoin_X, AlgHom.map_adjoin, Set.image_singleton, aeval_X]
 
 @[simp]
-theorem aeval_mem_adjoin_singleton : aeval x p ∈ adjoin R {x} := by
+theorem _root_.Polynomial.aeval_mem_adjoin_singleton : aeval x p ∈ adjoin R {x} := by
   simp [adjoin_singleton_eq_range_aeval]
 
-theorem _root_.Algebra.adjoin_mem_exists_aeval {a : A} (h : a ∈ Algebra.adjoin R {x}) :
+theorem adjoin_mem_exists_aeval {a : A} (h : a ∈ Algebra.adjoin R {x}) :
     ∃ p : R[X], aeval x p = a := by
   rw [Algebra.adjoin_singleton_eq_range_aeval] at h
   simp_all
 
-theorem _root_.Algebra.adjoin_eq_exists_aeval (a : Algebra.adjoin R {x}) :
+theorem adjoin_eq_exists_aeval (a : Algebra.adjoin R {x}) :
     ∃ p : R[X], aeval x p = a := by
   have : (a : A) ∈ Algebra.adjoin R {x} := by simp
   set y := (a : A) with h
   rw [Algebra.adjoin_singleton_eq_range_aeval] at this
   simp_all
 
+/--
+Proving a fact about `a : adjoin R {x}` is the same as proving it for
+`aeval x p` where `p`is an arbitrary polynomial. -/
 @[elab_as_elim]
-theorem _root_.Algebra.adjoin_singleton_induction {M : (adjoin R {x}) → Prop}
+theorem adjoin_singleton_induction {M : (adjoin R {x}) → Prop}
     (a : adjoin R {x}) (f : ∀ (p : Polynomial R),
     M (⟨aeval x p, aeval_mem_adjoin_singleton R x⟩ : adjoin R {x})) :
     M a := by
   obtain ⟨p, hp⟩ := Algebra.adjoin_eq_exists_aeval _ x a
   grind
 
 instance instCommSemiringAdjoinSingleton :
-    CommSemiring <| adjoin R {x} :=
-  { mul_comm := fun ⟨p, hp⟩ ⟨q, hq⟩ ↦ by
+    CommSemiring <| adjoin R {x} where
+  mul_comm := fun ⟨p, hp⟩ ⟨q, hq⟩ ↦ by
       obtain ⟨p', rfl⟩ := Algebra.adjoin_singleton_eq_range_aeval R x ▸ hp
       obtain ⟨q', rfl⟩ := Algebra.adjoin_singleton_eq_range_aeval R x ▸ hq
       simp only [AlgHom.toRingHom_eq_coe, RingHom.coe_coe, MulMemClass.mk_mul_mk, ← map_mul,
-        mul_comm p' q'] }
+        mul_comm p' q']
 
 instance instCommRingAdjoinSingleton {R A : Type*} [CommRing R] [Ring A] [Algebra R A] (x : A) :
-    CommRing <| Algebra.adjoin R {x} :=
-  { mul_comm := mul_comm }
+    CommRing <| Algebra.adjoin R {x} where
 
 end aeval
 
-end Polynomial
+end Algebra

Mathlib/RingTheory/Adjoin/Singleton.lean

@@ -5,7 +5,7 @@ Authors: Xavier Généreux, María Inés de Frutos Fernández
 -/
 module
 
-public import Mathlib.RingTheory.Adjoin.Polynomial
+public import Mathlib.RingTheory.Adjoin.Polynomial.Basic
 public import Mathlib.RingTheory.Polynomial.Tower
 /-!
 # Adjoin one single element

Mathlib/RingTheory/Algebraic/Basic.lean

@@ -6,7 +6,7 @@ Authors: Johan Commelin
 module
 
 public import Mathlib.Algebra.Polynomial.Expand
-public import Mathlib.RingTheory.Adjoin.Polynomial
+public import Mathlib.RingTheory.Adjoin.Polynomial.Basic
 public import Mathlib.RingTheory.Algebraic.Defs
 public import Mathlib.RingTheory.Polynomial.Tower
 public import Mathlib.RingTheory.Polynomial.UniqueFactorization

Mathlib/RingTheory/Algebraic/MvPolynomial.lean

@@ -6,7 +6,7 @@ Authors: Johan Commelin
 module
 
 public import Mathlib.Algebra.MvPolynomial.Supported
-public import Mathlib.RingTheory.Adjoin.Polynomial
+public import Mathlib.RingTheory.Adjoin.Polynomial.Basic
 public import Mathlib.RingTheory.Algebraic.Basic
 
 /-!

Mathlib/RingTheory/FiniteType.lean

@@ -6,7 +6,7 @@ Authors: Johan Commelin
 module
 
 public import Mathlib.Algebra.FreeAlgebra
-public import Mathlib.RingTheory.Adjoin.Polynomial
+public import Mathlib.RingTheory.Adjoin.Polynomial.Basic
 public import Mathlib.RingTheory.Adjoin.Tower
 public import Mathlib.RingTheory.Ideal.Quotient.Operations
 public import Mathlib.RingTheory.Noetherian.Orzech

Mathlib/RingTheory/IntegralClosure/IsIntegral/Basic.lean

@@ -7,7 +7,7 @@ module
 
 public import Mathlib.RingTheory.IntegralClosure.IsIntegral.Defs
 public import Mathlib.Algebra.Polynomial.Expand
-public import Mathlib.RingTheory.Adjoin.Polynomial
+public import Mathlib.RingTheory.Adjoin.Polynomial.Basic
 public import Mathlib.RingTheory.Finiteness.Subalgebra
 public import Mathlib.RingTheory.Polynomial.Tower
 

Mathlib/RingTheory/Polynomial/Ideal.lean

@@ -6,7 +6,7 @@ Authors: Kenny Lau
 module
 
 public import Mathlib.Algebra.Polynomial.RingDivision
-public import Mathlib.RingTheory.Adjoin.Polynomial
+public import Mathlib.RingTheory.Adjoin.Polynomial.Basic
 public import Mathlib.RingTheory.Ideal.Maps
 
 /-!