Theorems · Theorem · field theory

Field.Emb.Cardinal.filtration_succ

∀ {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)] [inst_3 : Algebra.IsAlgebraic F E]
  (i : (Module.rank F E).ord.ToType),
  IntermediateField.adjoin F
      (⇑(Field.Emb.Cardinal.wellOrderedBasis F E) ∘ Field.Emb.Cardinal.leastExt F E '' Set.Iio (Order.succ i)) =
    IntermediateField.restrictScalars F
      (↥(IntermediateField.adjoin F
            (⇑(Field.Emb.Cardinal.wellOrderedBasis F E) ∘ Field.Emb.Cardinal.leastExt F E ''
              Set.Iio i)))⟮(Field.Emb.Cardinal.wellOrderedBasis F E) (Field.Emb.Cardinal.leastExt F E i)⟯

Defined in

Mathlib.FieldTheory.CardinalEmb

Cited by

0 results in Mathlib

Foundations

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

Assumes

FieldFieldAlgebraFactAlgebra.IsAlgebraic