Commit 2024-11-28 12:19 1109970b

View on Github →

feat: IntermediateField.rank_sup_le (#19527) New results: In Mathlib/RingTheory/AlgebraicIndependent.lean:

  • IsTranscendenceBasis.lift_(cardinalMk|rank)_eq_max_lift: if x is a transcendence basis of E/F and is not empty, then [E:F] = #E = max(#F, #x, ℵ₀)
  • Algebra.Transcendental.rank_eq_cardinalMk: if E/F is transcendental, then [E:F] = #E. (a corollary of above result)
  • IntermediateField.rank_sup_le: if A and B are intermediate fields of E/F, then [AB:F] ≤ [A:F] * [B:F] (an application of above result) In Mathlib/RingTheory/Algebraic.lean:
  • [Algebra.]Transcendental.infinite: a ring has infinitely many elements if it has a transcendental element. In Mathlib/FieldTheory/MvRatFunc/Rank.lean (new file):
  • MvRatFunc.rank_eq_max_lift: rank of multivariate rational function field. Note that we don't have MvRatFunc yet, so the statement uses FractionRing (MvPolynomial ...). Eventually the theory of MvRatFunc should go this directory. Also move the results Algebra.IsAlgebraic.[lift_]cardinalMk_le_XXX from Mathlib/FieldTheory/IsAlgClosed/Classification.lean to a new file Mathlib/RingTheory/Algebraic/Cardinality.lean which has fewer imports.

Estimated changes