natDegree_minpolyDiv_succ
theorem natDegree_minpolyDiv_succ :
∀ {R : Type u_2} {S : Type u_1} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {x : S},
IsIntegral R x → ∀ [inst_3 : Nontrivial S], (minpolyDiv R x).natDegree + 1 = (minpoly R x).natDegree
The theorem `natDegree_minpolyDiv_succ` states that for any commutative rings `R` and `S`, with `S` being an `R`-algebra and `x` being an integral element over `R`, if `S` is nontrivial, then the natural degree of the polynomial obtained by dividing the minimal polynomial of `x` over `R` by `(X - C x)` (i.e., `minpolyDiv R x`), incremented by 1, is equal to the natural degree of the minimal polynomial of `x` over `R`. This theorem essentially relates the degrees of the minimal polynomial of `x` and the resulting polynomial after specific division.
More concisely: For any commutative rings R and S with S an R-algebra, and an integral element x in S over R with non-trivial S, the natural degrees of `minpoly x R` and `(minpoly x R) / (X - cx)` differ by at most 1.
|
minpolyDiv_spec
theorem minpolyDiv_spec :
∀ (R : Type u_2) {S : Type u_1} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (x : S),
minpolyDiv R x * (Polynomial.X - Polynomial.C x) = Polynomial.map (algebraMap R S) (minpoly R x)
This theorem states that for any commutative ring `R`, any commutative ring `S`, and any element `x` of `S`, where `S` is an algebra over `R`, the product of the function `minpolyDiv` applied to `R` and `x` and the polynomial `X - Cx` equals the mapping of the minimal polynomial of `R` and `x` under the algebraic map from `R` to `S`. Here, `minpolyDiv` is defined as the polynomial `minpoly R x / (X - C x)`. The `minpoly` is a polynomial of smallest degree that has `x` as a root. The `algebraMap` is an embedding from `R` to `S` given by the algebra structure. And `Polynomial.X` and `Polynomial.C x` represent the polynomial variable and the constant polynomial `x` respectively.
More concisely: For any commutative rings R and S, and any element x of S being an algebra element over R, the product of minpoly(R, x) / (X - Cx) and the algebra map from R to S equals the minimal polynomial of x over R.
|