# mathlib3documentation

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]
theorem omega.coeffs.val_between_nil {v : } {l : } (m : ) :
def omega.coeffs.val (v : ) (as : list ) :

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

Equations
@[simp]
theorem omega.coeffs.val_nil {v : } :
theorem omega.coeffs.val_between_eq_of_le {v : } {as : list } {l : } (m : ) :
as.length l + m l m = l (as.length - l)
theorem omega.coeffs.val_eq_of_le {v : } {as : list } {k : } :
as.length k as = 0 k
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 as = bs) l m = l m
theorem omega.coeffs.val_between_set {v : } {a : } {l n m : } :
l n n < l + m m = a * v n
@[simp]
theorem omega.coeffs.val_set {v : } {m : } {a : } :
= a * v m
theorem omega.coeffs.val_between_neg {v : } {as : list } {l o : } :
o = - l o
@[simp]
theorem omega.coeffs.val_neg {v : } {as : list } :
= - as
theorem omega.coeffs.val_between_add {v : } {is js : list } {l : } (m : ) :
js) l m = l m + l m
@[simp]
theorem omega.coeffs.val_add {v : } {is js : list } :
js) = is + js
theorem omega.coeffs.val_between_sub {v : } {is js : list } {l : } (m : ) :
js) l m = l m - l m
@[simp]
theorem omega.coeffs.val_sub {v : } {is js : list } :
js) = is - js
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 is = js) is = js
theorem omega.coeffs.val_except_update_set {v : } {n : } {as : list } {i j : } :
i v) as n) = as
theorem omega.coeffs.val_between_add_val_between {v : } {as : list } {l m n : } :
l m + (l + m) n = l (m + n)
theorem omega.coeffs.val_except_add_eq {v : } (n : ) {as : list } :
as + as * v n = as
@[simp]
theorem omega.coeffs.val_between_map_mul {v : } {i : } {as : list } {l m : } :
(list.map (has_mul.mul i) as) l m = i * l m
theorem omega.coeffs.forall_val_dvd_of_forall_mem_dvd {i : } {as : list } :
( (x : ), x as i x) (n : ), i as
theorem omega.coeffs.dvd_val_between {v : } {i : } {as : list } {l m : } :
( (x : ), x as i x) i l m
theorem omega.coeffs.dvd_val {v : } {as : list } {i : } :
( (x : ), x as i x) i as
@[simp]
theorem omega.coeffs.val_between_map_div {v : } {as : list } {i : } {l : } (h1 : (x : ), x as i x) {m : } :
(list.map (λ (x : ), x / i) as) l m = l m / i
@[simp]
theorem omega.coeffs.val_map_div {v : } {as : list } {i : } :
( (x : ), x as i x) (list.map (λ (x : ), x / i) as) = as / i
theorem omega.coeffs.val_between_eq_zero {v : } {is : list } {l m : } :
( (x : ), x is x = 0) l m = 0
theorem omega.coeffs.val_eq_zero {v : } {is : list } :
( (x : ), x is x = 0) is = 0