Polynomial.IsSeparableContraction.degree_eq
theorem Polynomial.IsSeparableContraction.degree_eq :
∀ {F : Type u_1} [inst : Field F] (q : ℕ) {f : Polynomial F} (hf : Polynomial.HasSeparableContraction q f)
[hF : ExpChar F q] (g : Polynomial F), Polynomial.IsSeparableContraction q f g → g.natDegree = hf.degree
The theorem `Polynomial.IsSeparableContraction.degree_eq` states that for any field `F` and any natural number `q`, if a polynomial `f` over `F` has a separable contraction (i.e., there exists a separable polynomial `g` such that `g(x^(q^m)) = f(x)` for some `m : ℕ`) and `F` has characteristic `q`, then the degree of any such separable contraction `g` equals the separable degree of `f`. In other words, the separable degree of a polynomial is unique.
More concisely: If a polynomial over a field of characteristic `q` has a separable contraction, then the degree of the separable contraction equals the separable degree of the polynomial.
|
Polynomial.IsSeparableContraction.dvd_degree'
theorem Polynomial.IsSeparableContraction.dvd_degree' :
∀ {F : Type u_1} [inst : CommSemiring F] {q : ℕ} {f : Polynomial F},
Polynomial.HasSeparableContraction q f →
∀ {g : Polynomial F}, Polynomial.IsSeparableContraction q f g → ∃ m, g.natDegree * q ^ m = f.natDegree
This theorem states that for any commutative semiring `F` and any natural number `q`, if a polynomial `f` over `F` has a separable contraction, then for any polynomial `g` that is a separable contraction of `f`, there exists a natural number `m` such that the degree of `g` times `q` raised to the power of `m` equals the degree of `f`. In other words, the degree of a separable contraction of a polynomial divides the degree of the original polynomial, with the factor of division being a power of the exponential characteristic of the semiring.
More concisely: For any commutative semiring `F` and natural numbers `q` and `m`, if polynomial `f` over `F` has a separable contraction `g`, then the degree of `g` times `q^m` equals the degree of `f` for some `m`.
|
Irreducible.hasSeparableContraction
theorem Irreducible.hasSeparableContraction :
∀ {F : Type u_1} [inst : Field F] (q : ℕ) [hF : ExpChar F q] {f : Polynomial F},
Irreducible f → Polynomial.HasSeparableContraction q f
This theorem states that, for every irreducible polynomial over a field, there exists a contraction to a separable polynomial. More formally, given a field `F`, a natural number `q` which is the exponential characteristic of `F`, and an irreducible polynomial `f` over `F`, then `f` satisfies the property of having a separable contraction with respect to `q`. This theorem is a part of the theory which describes the relationship between irreducible polynomials and separable polynomials.
More concisely: Given an irreducible polynomial `f` over a field `F` of characteristic `q`, there exists a separable polynomial `g` such that `g^q = f`.
|
Polynomial.HasSeparableContraction.dvd_degree
theorem Polynomial.HasSeparableContraction.dvd_degree :
∀ {F : Type u_1} [inst : CommSemiring F] {q : ℕ} {f : Polynomial F} (hf : Polynomial.HasSeparableContraction q f),
hf.degree ∣ f.natDegree
The theorem `Polynomial.HasSeparableContraction.dvd_degree` states that for any field `F` equipped with the structure of a commutative semiring, any natural number `q`, and any polynomial `f` of type `F`, if `f` has a separable contraction `hf`, then the degree of `hf` divides the natural degree of `f`. In other words, the degree of a separable contraction of a polynomial is always a divisor of the polynomial's degree.
More concisely: If `f` is a polynomial over a commutative semiring `F` with a separable contraction `hf`, then the degree of `hf` divides the degree of `f`.
|
Polynomial.HasSeparableContraction.eq_degree
theorem Polynomial.HasSeparableContraction.eq_degree :
∀ {F : Type u_1} [inst : CommSemiring F] {f : Polynomial F} (hf : Polynomial.HasSeparableContraction 1 f),
hf.degree = f.natDegree
This theorem states that in the case of a polynomial `f` over a commutative semiring `F`, which has a separable contraction of exponential characteristic one, the degree of this separable contraction equals the natural degree of the polynomial `f`. In simpler terms, for a given polynomial, if it contracts in a separable way at an exponential rate of one, its degree of contraction will match the polynomial's natural degree.
More concisely: For a polynomial `f` over a commutative semiring `F` with separable exponential characteristic one contraction, the degree of this contraction equals the natural degree of polynomial `f`.
|
Polynomial.contraction_degree_eq_or_insep
theorem Polynomial.contraction_degree_eq_or_insep :
∀ {F : Type u_1} [inst : Field F] (q : ℕ) [hq : NeZero q] [inst_1 : CharP F q] (g g' : Polynomial F) (m m' : ℕ),
(Polynomial.expand F (q ^ m)) g = (Polynomial.expand F (q ^ m')) g' →
g.Separable → g'.Separable → g.natDegree = g'.natDegree
The theorem `Polynomial.contraction_degree_eq_or_insep` states that for any field `F` of positive characteristic `q` which is not zero, and for any two separable polynomials `g` and `g'` in this field, if the expansion of `g` and `g'` by a factor of `q` raised to two different powers `m` and `m'` respectively are equal, then `g` and `g'` must have the same degree. Here, an expansion of a polynomial `p` by a factor of `n` transforms the polynomial `p = ∑ aₙ xⁿ` into `p' = ∑ aₙ xⁿⁿ`.
More concisely: For separable polynomials $g, g'\in F[x]$ over a field $F$ of positive characteristic $q$, if $(g)^q^m = (g')^q^{m'}$, then $\deg g = \deg g'$.
|
Polynomial.HasSeparableContraction.isSeparableContraction
theorem Polynomial.HasSeparableContraction.isSeparableContraction :
∀ {F : Type u_1} [inst : CommSemiring F] {q : ℕ} {f : Polynomial F} (hf : Polynomial.HasSeparableContraction q f),
Polynomial.IsSeparableContraction q f hf.contraction
This theorem states that if a polynomial `f` has a separable contraction over a commutative semiring `F` with respect to a natural number `q`, then the contraction of `f`, denoted as `hf.contraction`, is indeed a separable contraction. A separable contraction of a polynomial `f` is another polynomial `g` which is separable and has the property that `g(x^(q^m)) = f(x)` for some natural number `m`.
More concisely: If a polynomial `f` over a commutative semiring `F` has a separable contraction of degree `d` with respect to `q`, then the contraction `hf.contraction` is a separable polynomial of degree `d` over `F` that satisfies `(x^(q^m))^d = f(x)` for some natural number `m`.
|