Commit 2025-04-22 14:20 1eaa0105

feat(Algebra): transcendence degree is well-defined (#23539) In AlgebraicIndependent/TranscendenceBasis.lean, we show:

• The AlgebraicIndependent sets in a domain form a Matroid, which is used to show all transcendence bases have the same cardinality. Provide algebraic characterizations of the matroid notions Indep, Base, cRank, Basis, closure, Flat, and Spanning.
• Transcendence bases are exactly algebraic independent families that are spanning (i.e. the whole algebra is algebraic over the algebra generated by the family). On the other hand, a spanning set in a domain contains a transcendence basis.
• There always exists an transcendence basis between an arbitrary AlgebraicIndependent set and a spanning set in a domain.
• trdeg R S + trdeg S A = trdeg R A in a domain, which depends on AlgebraicIndependent/IsTranscendenceBasis.sumElim_comp.
• A finite AlgebraicIndependent family or spanning family in a domain that has the same cardinality as trdeg must be a transcendence basis.