Commit 2025-04-06 17:49 ba81780c

feat(Algebra): Transcendence degree (#20887) Define transcendence degree Algebra.trdeg and proves some basic properties: In AlgebraicIndependent/Basic.lean: define Algebra.trdeg to be the supremum of the cardinalities of all AlgebraicIndependent sets, just like Module.rank is defined to be the supremum of the cardinalities of all LinearIndependent sets. Add some API lemmas and trivial results about trdeg, e.g. that injective/surjective AlgHoms induce inequalities between trdegs, and AlgEquivs induce equalities. In AlgebraicIndependent/Transcendental.lean: add API lemmas and show the inequality trdeg R S + trdeg S A ≤ trdeg R A (which does not require a domain). In AlgebraicIndependent/Defs.lean: add Stacks tags and some trivial API lemmas about IsTranscendenceBasis. Thanks to Chris Hughes and Jz Pan for preliminary works and Peter Nelson for the hint about Finitary and IndepMatroid. TODO:

• The analogue of StrongRankCondition in the setting of algebras, which implies trdeg R (MvPolynomial (Fin n) R) = n for all Nontrivial CommRing R.