Commit 2026-03-01 10:55 ce269e54

View on Github →

chore(RingTheory/Adjoin/Polynomial): move to Basic.lean (#35883) Future changes in #35864 will add a new file Transcendental.lean.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Polynomial/Derivation.lean

Renamed Mathlib/RingTheory/Adjoin/Polynomial.lean to Mathlib/RingTheory/Adjoin/Polynomial/Basic.lean

modified theorem Algebra.adjoin_eq_exists_aeval

modified theorem Algebra.adjoin_mem_exists_aeval

modified theorem Algebra.adjoin_singleton_eq_range_aeval

modified theorem Algebra.adjoin_singleton_induction

modified theorem Polynomial.adjoin_X

modified theorem Polynomial.aeval_mem_adjoin_singleton

Modified Mathlib/RingTheory/Adjoin/Singleton.lean

Modified Mathlib/RingTheory/Algebraic/Basic.lean

Modified Mathlib/RingTheory/Algebraic/MvPolynomial.lean

Modified Mathlib/RingTheory/FiniteType.lean

Modified Mathlib/RingTheory/IntegralClosure/IsIntegral/Basic.lean

Modified Mathlib/RingTheory/Polynomial/Ideal.lean