Separable degree #
This file contains basics about the separable degree of a polynomial.
Main results #
IsSeparableContraction: is the condition that, for
ga separable polynomial, we have that
g(x^(q^m)) = f(x)for some
m : ℕ.
HasSeparableContraction: the condition of having a separable contraction
HasSeparableContraction.degree: the separable degree, defined as the degree of some separable contraction
Irreducible.HasSeparableContraction: any irreducible polynomial can be contracted to a separable polynomial
HasSeparableContraction.dvd_degree': the degree of a separable contraction divides the degree, in function of the exponential characteristic of the field
HasSeparableContraction.eq_degreespecialize the statement of
IsSeparableContraction.degree_eq: the separable degree is well-defined, implemented as the statement that the degree of any separable contraction equals
separable degree, degree, polynomial
The separable degree divides the degree, in function of the exponential characteristic of F.
Every irreducible polynomial can be contracted to a separable polynomial. https://stacks.math.columbia.edu/tag/09H0
If two expansions (along the positive characteristic) of two separable polynomials
agree, then they have the same degree.
The separable degree equals the degree of any separable contraction, i.e., it is unique.