mathlib documentation

tactic.omega.lin_comb

@[simp]

Linear combination of constraints. The second argument is the list of constraints, and the first argument is the list of conefficients by which the constraints are multiplied

Equations
theorem omega.lin_comb_holds {v : } {ts : list omega.term} (ns : list ) :
(∀ (t : omega.term), t ts0 omega.term.val v t)0 omega.term.val v (omega.lin_comb ns ts)
def omega.unsat_lin_comb (ns : list ) (ts : list omega.term) :
Prop

unsat_lin_comb ns ts asserts that the linear combination lin_comb ns ts is unsatisfiable

Equations
theorem omega.unsat_lin_comb_of (ns : list ) (ts : list omega.term) :
(omega.lin_comb ns ts).fst < 0(∀ (x : ), x (omega.lin_comb ns ts).sndx = 0)omega.unsat_lin_comb ns ts