Theorems · Definition · field theory
Field.finSepDegree
(F : Type u) → (E : Type v) → [inst : Field F] → [inst_1 : Field E] → [Algebra F E] → ℕ
If E / F is an algebraic extension, then the (finite) separable degree of E / F
is the number of F-algebra homomorphisms from E to the algebraic closure of E,
as a natural number. It is defined to be zero if there are infinitely many of them.
Note that if E / F is not algebraic, then this definition makes no mathematical sense.
- Defined in
- Mathlib.FieldTheory.SeparableDegree
- Cited by
- 24 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.
Cites4
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
Cited by24
Results whose statement or proof uses this declaration.
- Field.finSepDegree_eq_finrank_of_isSeparablestatement and proof · cited by 7
- Field.finSepDegree_mul_finSepDegree_of_isAlgebraicstatement · cited by 6
- IntermediateField.finSepDegree_adjoin_simple_eq_finrank_iffstatement · cited by 4
- IsSeparable.of_algebra_isSeparable_of_isSeparableproof · cited by 3
- Field.finSepDegree_eq_of_equivstatement · cited by 3
- IntermediateField.finSepDegree_botstatement · cited by 2
- isPurelyInseparable_iff_finSepDegree_eq_onestatement and proof · cited by 2
- IsPurelyInseparable.finSepDegree_eq_onestatement · cited by 2
- Field.finSepDegree_eqstatement and proof · cited by 2
- Field.finSepDegree_eq_finrank_iffstatement and proof · cited by 2
- IntermediateField.finSepDegree_topstatement · cited by 2
- Field.finSepDegree_selfstatement · cited by 1