Commit 2024-11-30 09:21 ad2e8f11

chore(RingTheory): split up Algebraic.lean (#19370) Split up the file RingTheory/Algebraic.lean into a few subfiles:

• Algebraic/Defs.lean: definition of algebraic and transcendental elements and (sub)algebras
• Algebraic/Integral.lean: relate IsAlgebraic and IsIntegral
• Algebraic/Basic.lean: most results on showing certain elements are algebraic (this is probably the file you want to import afterwards)
• Algebraic/LinearIndependent.lean: showing certain families are linear independent using transcendentality
• Algebraic/MvPolynomial.lean: results on multivariate polynomials
• Algebraic/Pi.lean: a definition of algebraic function (which seems to be unused otherwise). See also [mathlib3#11156](https://github.com/leanprover-community/mathlib3/pull/11156). I don't expect a particularly exciting import reduction, but it does clean up the file structure somewhat, in particular by moving the relation between algebraic and integral elements to one dedicated place (which had been irritating me for years!).