Theorems · Definition · field theory
Field.Emb.Cardinal.filtration
{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] → WithTop (Module.rank F E).ord.ToType ↪o IntermediateField F EExtend the family E⟮<i⟯, i : ι by adjoining a top element.
- Defined in
- Mathlib.FieldTheory.CardinalEmb
- Cited by
- 7 results in Mathlib
- Foundations
- Depth 151 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites21
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coeproof · cited by 62,936
- Algebrastatement and proof · cited by 11,388
- Top.topproof · cited by 9,680
- Fieldstatement and proof · cited by 7,404
- Set.imageproof · cited by 5,609
- WithTopstatement and proof · cited by 3,754
- Factstatement and proof · cited by 2,726
- Cardinalstatement · cited by 2,598
- Set.Iioproof · cited by 1,166
- IntermediateFieldstatement · cited by 988
- OrderEmbeddingstatement · cited by 619
- Cardinal.aleph0statement and proof · cited by 521
Cited by11
Results whose statement or proof uses this declaration.
- Field.Emb.Cardinal.embFunctorstatement and proof · cited by 3
- Field.Emb.Cardinal.embEquivPiproof · cited by 1
- Field.Emb.Cardinal.equivLimstatement and proof · cited by 1
- Field.Emb.Cardinal.equivSuccstatement and proof · cited by 1
- Field.Emb.Cardinal.embFunctor.congr_simpstatement and proof · cited by 0
- Field.Emb.Cardinal.directed_filtrationstatement and proof · cited by 0
- Field.Emb.Cardinal.eq_bot_of_not_nonemptystatement · cited by 0
- Field.Emb.Cardinal.equivLim_coherencestatement and proof · cited by 0
- Field.Emb.Cardinal.equivSucc_coherencestatement and proof · cited by 0
- Field.Emb.Cardinal.filtration_applystatement · cited by 0
- Field.Emb.Cardinal.iSup_filtrationstatement and proof · cited by 0