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
: ifx
is a transcendence basis ofE/F
and is not empty, then[E:F] = #E = max(#F, #x, ℵ₀)
Algebra.Transcendental.rank_eq_cardinalMk
: ifE/F
is transcendental, then[E:F] = #E
. (a corollary of above result)IntermediateField.rank_sup_le
: ifA
andB
are intermediate fields ofE/F
, then[AB:F] ≤ [A:F] * [B:F]
(an application of above result) InMathlib/RingTheory/Algebraic.lean
:[Algebra.]Transcendental.infinite
: a ring has infinitely many elements if it has a transcendental element. InMathlib/FieldTheory/MvRatFunc/Rank.lean
(new file):MvRatFunc.rank_eq_max_lift
: rank of multivariate rational function field. Note that we don't haveMvRatFunc
yet, so the statement usesFractionRing (MvPolynomial ...)
. Eventually the theory ofMvRatFunc
should go this directory. Also move the resultsAlgebra.IsAlgebraic.[lift_]cardinalMk_le_XXX
fromMathlib/FieldTheory/IsAlgClosed/Classification.lean
to a new fileMathlib/RingTheory/Algebraic/Cardinality.lean
which has fewer imports.