Commit 2024-10-18 14:51 c289ac29

feat(RingTheory/Algebraic): add some results on Transcendental (#17867)

• transcendental_iff, transcendental_iff_ker_eq_bot: similar to the API of AlgebraicIndependent
• IsAlgebraic.of_aeval, Transcendental.aeval: behavior of transcendental over aeval
• Polynomial.transcendental, Polynomial.transcendental_X: some specific polynomials are transcendental over its base ring
• Transcendental.linearIndependent_sub_inv: if E / F is a field extension, x is an element of E transcendental over F, then {(x - a)⁻¹ | a : F} is linearly independent over F
• transcendental_algebraMap_iff: negation of isAlgebraic_algebraMap_iff