The degree of rational functions

Main definitions

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

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

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

• x.intDegree = ↑x.num.natDegree - ↑x.denom.natDegree

@[simp]

theorem RatFunc.intDegree_zero {K : Type u} [Field K] : RatFunc.intDegree 0 = 0

@[simp]

theorem RatFunc.intDegree_one {K : Type u} [Field K] : RatFunc.intDegree 1 = 0

@[simp]

theorem RatFunc.intDegree_C {K : Type u} [Field K] (k : K) : (RatFunc.C k).intDegree = 0

@[simp]

theorem RatFunc.intDegree_X {K : Type u} [Field K] : RatFunc.X.intDegree = 1

@[simp]

theorem RatFunc.intDegree_polynomial {K : Type u} [Field K] {p : Polynomial K} : ((algebraMap (Polynomial K) (RatFunc K)) p).intDegree = ↑p.natDegree

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

@[simp]

theorem RatFunc.intDegree_neg {K : Type u} [Field K] (x : RatFunc K) : (-x).intDegree = x.intDegree

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

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

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