Theorems · Definition · field theory
separableClosure
(F : Type u) → (E : Type v) → [inst : Field F] → [inst_1 : Field E] → [inst_2 : Algebra F E] → IntermediateField F E
The (relative) separable closure of F in E, or called maximal separable subextension
of E / F, is defined to be the intermediate field of E / F consisting of all separable
elements. The previous results prove that these elements are closed under field operations.
- Defined in
- Mathlib.FieldTheory.SeparableClosure
- Cited by
- 55 results in Mathlib
- Foundations
- Depth 193 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites8
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
- Set.ofPredproof · cited by 6,101
- IntermediateFieldstatement · cited by 988
- IsSeparableproof · cited by 68
- Field.isSeparable_mulproof · cited by 0
- Field.isSeparable_addproof · cited by 0
- Field.isSeparable_invproof · cited by 0
Cited by62
Results whose statement or proof uses this declaration.
- Field.sepDegreeproof · cited by 24
- Field.insepDegreeproof · cited by 23
- Field.finInsepDegreeproof · cited by 15
- mem_separableClosure_iffstatement · cited by 7
- separableClosure.eq_top_iffstatement and proof · cited by 6
- AlgEquiv.separableClosurestatement · cited by 4
- separableClosure.le_restrictScalarsstatement · cited by 4
- separableClosure.separableClosure_eq_botstatement and proof · cited by 3
- map_mem_separableClosure_iffstatement · cited by 3
- separableClosure.eq_bot_of_isPurelyInseparablestatement and proof · cited by 3
- le_separableClosurestatement · cited by 2
- Algebra.trace_eq_zero_of_not_isSeparableproof · cited by 2