Theorems · Definition · field theory
Field.Emb.Cardinal.factor
{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 → Type vExtend the family X i := E⟮<i⟯ →ₐ[F] Ē from ι to WithTop ι.
- Defined in
- Mathlib.FieldTheory.CardinalEmb
- Cited by
- 2 results in Mathlib
- Foundations
- Depth 177 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites18
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
- 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
- Cardinal.aleph0statement and proof · cited by 521
- Module.rankstatement and proof · cited by 496
- IntermediateField.adjoinproof · cited by 382
- Algebra.IsAlgebraicstatement and proof · cited by 322
Cited by4
Results whose statement or proof uses this declaration.
- Field.Emb.cardinal_eq_two_pow_rankproof · cited by 2
- Field.Emb.Cardinal.embEquivPistatement and proof · cited by 1
- Field.Emb.Cardinal.equivSuccstatement · cited by 1
- Field.Emb.Cardinal.equivSucc_coherencestatement · cited by 0