Theorems · Definition · field theory

Field.Emb.Cardinal.equivSucc

{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 : WithTop (Module.rank F E).ord.ToType) →
                (↥(Field.Emb.Cardinal.filtration (Order.succ i)) →ₐ[F] AlgebraicClosure E) ≃
                  (↥(Field.Emb.Cardinal.filtration i) →ₐ[F] AlgebraicClosure E) × Field.Emb.Cardinal.factor i

Extend succEquiv from ι to WithTop ι.

Defined in

Mathlib.FieldTheory.CardinalEmb

Cited by

1 results in Mathlib

Foundations

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

Assumes

FieldFieldAlgebraFactAlgebra.IsAlgebraic