Commit 2026-09-21 10:54 6747d291

feat(Adjoin/Polynomial/Transcendental): Adjoining transcendental elements (#37723) This PR establishes some basic properties about A[y] when y is transcendental over A. These are mostly just carried over from A[X].

• Move algEquivOfTranscendental in the newly created file Mathlib.RingTheory.Adjoin.Polynomial.Transcendental
• Add Algebra.adjoin.evalOfTranscendental. This is technically very similar to Algebra.adjoin.liftSingleton but the definition is much simpler. It is also currently more general in the sense that it doesn't require A to be a field.
• Some basic instances from Polynomial. Note that these are actually theorems because of the hypothesis (h : Transcendental R s) everywhere. I've also added a Fact version to allow the possibility of instances. Last note : I initially considered adding some results in RingTheory.Polynomial.Quotient where I golfed the file a tiny bit. I removed the unused results but kept the golf. AI disclaimer : I used Claude to give me some feedback on the PR.