Theorems · Definition · field theory

Field.Emb.Cardinal.leastExt

(F : Type u) →
  (E : Type v) →
    [inst : Field F] →
      [inst_1 : Field E] →
        [inst_2 : Algebra F E] →
          [rank_inf : Fact (Cardinal.aleph0 ≤ Module.rank F E)] →
            [Algebra.IsAlgebraic F E] → (Module.rank F E).ord.ToType → (Module.rank F E).ord.ToType

leastExt i is defined to be the smallest k : ι that generates a nontrivial extension over (i.e. does not lie in) the subalgebra (= intermediate field) generated by all previous leastExt j, j < i. For cardinality reasons, such k always exist if ι is infinite.

Defined in

Mathlib.FieldTheory.CardinalEmb

Cited by

13 results in Mathlib

Foundations

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

Assumes

FieldFieldAlgebraFactAlgebra.IsAlgebraic