Documentation

Mathlib.FieldTheory.RatFunc.Degree

The degree of rational functions #

Main definitions #

We define the degree of a rational function, with values in ℤ:

source
def RatFunc.intDegree {K : Type u} [Field K] (x : RatFunc K) :
ℤ

intDegree x is the degree of the rational function x, defined as the difference between the natDegree of its numerator and the natDegree of its denominator. In particular, intDegree 0 = 0.

Equations
Instances For
    source
    @[simp]
    theorem RatFunc.intDegree_zero {K : Type u} [Field K] :
    intDegree 0 = 0
    source
    @[simp]
    theorem RatFunc.intDegree_one {K : Type u} [Field K] :
    intDegree 1 = 0
    source
    @[simp]
    theorem RatFunc.intDegree_C {K : Type u} [Field K] (k : K) :
    (C k).intDegree = 0
    source
    @[simp]
    theorem RatFunc.intDegree_X {K : Type u} [Field K] :
    X.intDegree = 1
    source
    @[simp]
    theorem RatFunc.intDegree_polynomial {K : Type u} [Field K] {p : Polynomial K} :
    ((algebraMap (Polynomial K) (RatFunc K)) p).intDegree = ↑p.natDegree
    source
    theorem RatFunc.intDegree_mul {K : Type u} [Field K] {x y : RatFunc K} (hx : x ≠ 0) (hy : y ≠ 0) :
    (x * y).intDegree = x.intDegree + y.intDegree
    source
    @[simp]
    theorem RatFunc.intDegree_neg {K : Type u} [Field K] (x : RatFunc K) :
    (-x).intDegree = x.intDegree
    source
    theorem RatFunc.intDegree_add {K : Type u} [Field K] {x y : RatFunc K} (hxy : x + y ≠ 0) :
    (x + y).intDegree = ↑(x.num * y.denom + x.denom * y.num).natDegree - ↑(x.denom * y.denom).natDegree
    source
    theorem RatFunc.natDegree_num_mul_right_sub_natDegree_denom_mul_left_eq_intDegree {K : Type u} [Field K] {x : RatFunc K} (hx : x ≠ 0) {s : Polynomial K} (hs : s ≠ 0) :
    ↑(x.num * s).natDegree - ↑(s * x.denom).natDegree = x.intDegree
    source
    theorem RatFunc.intDegree_add_le {K : Type u} [Field K] {x y : RatFunc K} (hy : y ≠ 0) (hxy : x + y ≠ 0) :
    (x + y).intDegree ≤ x.intDegree ⊔ y.intDegree