mathlib3 documentation

tactic.omega.coeffs

@[simp]
def omega.coeffs.val_between (v : ) (as : list ) (l : ) :

val_between v as l o is the value (under valuation v) of the term obtained taking the term represented by (0, as) and dropping all subterms that include variables outside the range [l,l+o)

Equations
@[simp]
def omega.coeffs.val (v : ) (as : list ) :

Evaluation of the nonconstant component of a normalized linear arithmetic term.

Equations
theorem omega.coeffs.val_between_eq_val_between {v w : } {as bs : list } {l m : } :
( (x : ), l x x < l + m v x = w x) ( (x : ), l x x < l + m list.func.get x as = list.func.get x bs) omega.coeffs.val_between v as l m = omega.coeffs.val_between w bs l m
theorem omega.coeffs.val_between_set {v : } {a : } {l n m : } :
@[simp]
theorem omega.coeffs.val_set {v : } {m : } {a : } :
def omega.coeffs.val_except (k : ) (v : ) (as : list ) :

val_except k v as is the value (under valuation v) of the term obtained taking the term represented by (0, as) and dropping the subterm that includes the kth variable.

Equations
theorem omega.coeffs.val_except_eq_val_except {k : } {is js : list } {v w : } :
( (x : ), x k v x = w x) ( (x : ), x k list.func.get x is = list.func.get x js) omega.coeffs.val_except k v is = omega.coeffs.val_except k w js
@[simp]
theorem omega.coeffs.forall_val_dvd_of_forall_mem_dvd {i : } {as : list } :
( (x : ), x as i x) (n : ), i list.func.get n as
theorem omega.coeffs.dvd_val_between {v : } {i : } {as : list } {l m : } :
( (x : ), x as i x) i omega.coeffs.val_between v as l m
theorem omega.coeffs.dvd_val {v : } {as : list } {i : } :
( (x : ), x as i x) i omega.coeffs.val v as
@[simp]
theorem omega.coeffs.val_between_map_div {v : } {as : list } {i : } {l : } (h1 : (x : ), x as i x) {m : } :
omega.coeffs.val_between v (list.map (λ (x : ), x / i) as) l m = omega.coeffs.val_between v as l m / i
@[simp]
theorem omega.coeffs.val_map_div {v : } {as : list } {i : } :
( (x : ), x as i x) omega.coeffs.val v (list.map (λ (x : ), x / i) as) = omega.coeffs.val v as / i
theorem omega.coeffs.val_between_eq_zero {v : } {is : list } {l m : } :
( (x : ), x is x = 0) omega.coeffs.val_between v is l m = 0
theorem omega.coeffs.val_eq_zero {v : } {is : list } :
( (x : ), x is x = 0) omega.coeffs.val v is = 0