Theorems · Definition · field theory
IntermediateField.botEquiv
(F : Type u_1) → [inst : Field F] → (E : Type u_2) → [inst_1 : Field E] → [inst_2 : Algebra F E] → ↥⊥ ≃ₐ[F] F
The bottom IntermediateField is isomorphic to the field.
- Cited by
- 14 results in Mathlib
- Foundations
- Depth 86 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites10
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
- Fieldstatement and proof · cited by 7,404
- Bot.botstatement and proof · cited by 4,720
- AlgEquivstatement · cited by 1,681
- IntermediateFieldstatement · cited by 988
- IntermediateField.toSubalgebraproof · cited by 134
- AlgEquiv.transproof · cited by 108
- Subalgebra.equivOfEqproof · cited by 15
- Algebra.botEquivproof · cited by 4
- IntermediateField.bot_toSubalgebraproof · cited by 2
Cited by15
Results whose statement or proof uses this declaration.
- Field.nonempty_algHom_of_exists_rootproof · cited by 3
- IntermediateField.finSepDegree_botproof · cited by 2
- Field.Emb.Cardinal.equivLimproof · cited by 1
- IntermediateField.lift_insepDegree_bot'proof · cited by 1
- IntermediateField.botEquiv_defstatement and proof · cited by 0
- IntermediateField.botEquiv_symmstatement · cited by 0
- IntermediateField.insepDegree_bot'proof · cited by 0
- IntermediateField.isSeparable_botproof · cited by 0
- IntermediateField.coe_algebraMap_over_botstatement · cited by 0
- IntermediateField.sepDegree_botproof · cited by 0
- IntermediateField.sepDegree_bot'proof · cited by 0
- IntermediateField.lift_sepDegree_bot'proof · cited by 0