Theorems · Definition · field theory

Field.Emb.Cardinal.succEquiv

{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))) →ₐ[F]
                    AlgebraicClosure E) ≃
                  (↥(IntermediateField.adjoin F
                          (⇑(Field.Emb.Cardinal.wellOrderedBasis F E) ∘ Field.Emb.Cardinal.leastExt F E ''
                            Set.Iio i)) →ₐ[F]
                      AlgebraicClosure E) ×
                    Field.Emb
                      ↥(IntermediateField.adjoin F
                          (⇑(Field.Emb.Cardinal.wellOrderedBasis F E) ∘ Field.Emb.Cardinal.leastExt F E '' Set.Iio i))
                      ↥(↥(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)⟯

Each embedding of E⟮<i⟯ into Ē extend to #(X i) embeddings of E⟮<i⁺⟯.

Defined in

Mathlib.FieldTheory.CardinalEmb

Cited by

1 results in Mathlib

Foundations

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

Assumes

FieldFieldAlgebraFactAlgebra.IsAlgebraic