Theorems · Theorem · field theory

IsAlgClosed.cardinal_le_max_transcendence_basis

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

The cardinality of an algebraically closed R-algebra is less than or equal to the maximum of the cardinality of R, the cardinality of a transcendence basis and ℵ₀ For a simpler, but less universe-polymorphic statement, see IsAlgClosed.cardinal_le_max_transcendence_basis'

Defined in

Mathlib.FieldTheory.IsAlgClosed.Classification

Cited by

2 results in Mathlib

Foundations

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

Assumes

CommRingFieldAlgebraIsAlgClosed