Mathlib Map

Theorems · Theorem · field theory

Field.Emb.Cardinal.eq_bot_of_not_nonempty

∀ {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},
  Order.IsSuccPrelimit i → ¬Nonempty ↑(Set.Iio i) → Field.Emb.Cardinal.filtration i = ⊥
Defined in
Mathlib.FieldTheory.CardinalEmb
Cited by
0 results in Mathlib
Foundations
Depth 152 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes
FieldFieldAlgebraFactAlgebra.IsAlgebraic
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Field.Emb.Cardinal.equivLim · cited by 1Cardinal.equivLimDFunLike.coe · cited by 62936DFunLike.coeSet · cited by 53352SetAlgebra · cited by 11388AlgebraTop.top · cited by 9680Top.topSetLike.coe · cited by 8199SetLike.coeField · cited by 7404FieldSet.Elem · cited by 7166Set.ElemSet.image · cited by 5609Set.imageBot.bot · cited by 4720Bot.botWithTop · cited by 3754WithTopFact · cited by 2726FactCardinal · cited by 2598CardinalLT.lt.ne' · cited by 1417lt.ne'Set.Iio · cited by 1166Set.IioWithTop.some · cited by 1128WithTop.someCardinal.eq_bot_of_not_nonemp…CITED BYCITES

Cites35

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

  • DFunLike.coestatement and proof · cited by 62,936
  • Setproof · cited by 53,352
  • Algebrastatement and proof · cited by 11,388
  • Top.topproof · cited by 9,680
  • SetLike.coeproof · cited by 8,199
  • Fieldstatement and proof · cited by 7,404
  • Set.Elemstatement and proof · cited by 7,166
  • Set.imageproof · cited by 5,609
  • Bot.botstatement and proof · cited by 4,720
  • WithTopstatement and proof · cited by 3,754
  • Factstatement and proof · cited by 2,726
  • Cardinalstatement · cited by 2,598

Cited by1

Results whose statement or proof uses this declaration.