mathlib documentation

tactic.omega.coeffs

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

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

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

Equations
@[simp]

theorem omega.coeffs.val_between_eq_of_le {v : } {as : list } {l : } (m : ) :

theorem omega.coeffs.val_eq_of_le {v : } {as : list } {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 + mlist.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 : } :
l nn < l + momega.coeffs.val_between v list.nil {n a} l m = a * v n

@[simp]
theorem omega.coeffs.val_set {v : } {m : } {a : } :

@[simp]

@[simp]

@[simp]

def omega.coeffs.val_except  :
()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 kv x = w x)(∀ (x : ), x klist.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.val_between_map_mul {v : } {i : } {as : list } {l m : } :

theorem omega.coeffs.forall_val_dvd_of_forall_mem_dvd {i : } {as : list } (a : ∀ (x : ), x asi x) (n : ) :

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

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

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

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