# mathlibdocumentation

tactic.omega.coeffs

@[simp]
def omega.coeffs.val_between  :
()

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  :
()

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 xx < l + mv x = w x)(∀ (x : ), l xx < l + m as = bs) l m = l m

theorem omega.coeffs.val_between_set {v : } {a : } {l n m : } :
l nn < l + m l 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  :
()

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 kv x = w x)(∀ (x : ), x k is = js) is = js

theorem omega.coeffs.val_except_update_set {v : } {n : } {as : list } {i j : } :
v n i as {n j} = 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 } (a : ∀ (x : ), x asi x) (n : ) :
i as

theorem omega.coeffs.dvd_val_between {v : } {i : } {as : list } {l m : } :
(∀ (x : ), x asi x)i l m

theorem omega.coeffs.dvd_val {v : } {as : list } {i : } :
(∀ (x : ), x asi x)i as

@[simp]
theorem omega.coeffs.val_between_map_div {v : } {as : list } {i : } {l : } (h1 : ∀ (x : ), x asi 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 asi x) (list.map (λ (x : ), x / i) as) = as / i

theorem omega.coeffs.val_between_eq_zero {v : } {is : list } {l m : } :
(∀ (x : ), x isx = 0) l m = 0

theorem omega.coeffs.val_eq_zero {v : } {is : list } :
(∀ (x : ), x isx = 0) is = 0