theorem transcendence_basis_lift_cardinalMk_eq {k : Type u_2} {L : Type u_3} [Field k] [Field L] [Algebra k L] {ι : Type u} {ι' : Type v} {x : ι → L} {y : ι' → L} (hx : IsTranscendenceBasis k x) (hy : IsTranscendenceBasis k y) : Cardinal.lift.{v, u} (Cardinal.mk ι) = Cardinal.lift.{u, v} (Cardinal.mk ι')

Any two transcendence bases of a field extension $L/k$ have the same cardinality (up to universe lifts).

@[reducible, inline]

noncomputable abbrev transcendenceDegree (k : Type u_2) (L : Type u_3) [Field k] [Field L] [Algebra k L] : Cardinal.{u_3}

The transcendence degree of a field extension $L/k$: the cardinality of any transcendence basis.

@[reducible, inline]

noncomputable abbrev krullDimension (R : Type u_1) [CommSemiring R] : WithBot ℕ∞

The Krull dimension of a commutative semiring: the supremum of lengths of chains of prime ideals.

theorem krullDim_eq_trdeg_fractionField (k : Type u_1) [Field k] (R : Type u_2) [CommRing R] [IsDomain R] [Algebra k R] [Algebra.FiniteType k R] : krullDimension R = ↑(Cardinal.toENat (Algebra.trdeg k (FractionRing R)))

For a finitely generated $k$-algebra domain $R$, the Krull dimension equals the transcendence degree of its fraction field over $k$.