Theorems · Theorem · field theory
IntermediateField.adjoin_univ
∀ (F : Type u_3) (E : Type u_4) [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E], IntermediateField.adjoin F Set.univ = ⊤
- Cited by
- 6 results in Mathlib
- Foundations
- Depth 85 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites9
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Algebrastatement and proof · cited by 11,388
- Top.topstatement and proof · cited by 9,680
- SetLike.coeproof · cited by 8,199
- Fieldstatement and proof · cited by 7,404
- Set.univstatement · cited by 3,945
- IntermediateFieldstatement · cited by 988
- IntermediateField.adjoinstatement · cited by 382
- eq_top_iffproof · cited by 236
- IntermediateField.subset_adjoinproof · cited by 59
Cited by7
Results whose statement or proof uses this declaration.
- IntermediateField.exists_algHom_of_splits_of_aevalproof · cited by 4
- IntermediateField.exists_algHom_of_splits'proof · cited by 2
- Field.embEquivOfIsAlgClosedproof · cited by 1
- Polynomial.irreducible_compproof · cited by 1
- IntermediateField.nonempty_algHom_of_splitsproof · cited by 0
- Field.span_map_pow_expChar_pow_eq_top_of_isSeparableproof · cited by 0
- IntermediateField.exists_algHom_of_splitsproof · cited by 0