Commit 2026-08-10 08:17 6cf26736

View on Github →

feat(FieldTheory): typeclass for field extension with finite transcendence degree (#42152) Make a new typeclass for field extensions with finite transcendence degree. See Zulip.

Estimated changes

Modified Mathlib.lean

Created Mathlib/FieldTheory/FinTrdeg.lean

added theorem FinTrdeg.of_isTranscendenceBasis

added theorem FinTrdeg.trans

added theorem exists_finset_isTranscendenceBasis

added theorem finTrdeg_iff_trdeg

added theorem finite_of_algebraicIndependent

added theorem finite_of_isTranscendenceBasis

added theorem trdeg_lt_aleph0

Modified Mathlib/FieldTheory/IntermediateField/Adjoin/Basic.lean

Modified Mathlib/RingTheory/AlgebraicIndependent/TranscendenceBasis.lean

deleted theorem trdeg_lt_aleph0

added theorem trdeg_lt_aleph0_of_finiteType