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
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).snd x = 0) omega.unsat_lin_comb ns ts