mathlib3 documentation

tactic.omega.nat.dnf

DNF transformation #

Return a list of bools that encodes which variables have nonzero coefficients

Equations

Return a list of bools that encodes which variables have nonzero coefficients in any one of the input terms.

Equations
theorem omega.nat.holds_nonneg_consts_core {v : } (h1 : (x : ), 0 v x) (m : ) (bs : list bool) (t : omega.term) (H : t omega.nat.nonneg_consts_core m bs) :