Theorems · Theorem · field theory

IsAlgClosed.cardinal_eq_cardinal_transcendence_basis_of_aleph0_lt

∀ {R : Type u} {K : Type v} [inst : CommRing R] [inst_1 : Field K] [inst_2 : Algebra R K] [IsAlgClosed K] {ι : Type w}
  (v : ι → K) [Nontrivial R],
  IsTranscendenceBasis R v →
    Cardinal.mk R ≤ Cardinal.aleph0 →
      Cardinal.aleph0 < Cardinal.mk K → Cardinal.lift.{w, v} (Cardinal.mk K) = Cardinal.lift.{v, w} (Cardinal.mk ι)

If K is an uncountable algebraically closed field, then its cardinality is the same as that of a transcendence basis. For a simpler, but less universe-polymorphic statement, see IsAlgClosed.cardinal_eq_cardinal_transcendence_basis_of_aleph0_lt'

Defined in

Mathlib.FieldTheory.IsAlgClosed.Classification

Cited by

2 results in Mathlib

Foundations

Depth 138 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommRingFieldAlgebraIsAlgClosedNontrivial