English
finSepDegree F E is the natural number counting F-embeddings of E into the algebraic closure of E; it is defined to be zero if there are infinitely many embeddings.
Русский
finSepDegree F E — это натуральное число, равное числу F-встраиваний E в алгебраическое замыкание E; при бесконечном числе встраиваний задаётся нулём.
LaTeX
$$$\\operatorname{finSepDegree} F E = \\#(\\mathrm{Emb} F E)$$$
Lean4
/-- 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. -/
def finSepDegree : ℕ :=
Nat.card (Emb F E)
