Reference · Signed rationals

rainbow.math.rational.signed.no-zero-divisors

Signed rationalssrc/rainbow/math/rational/signed/no_zero_divisors.clj0 definitions, 3 theorems

No-zero-divisors sub-foundation for strict convexity: nonzero facts and (building up) a != 0 -> b != 0 -> a*b != 0. Brick 1 first: 1 !~ 0.

Depends onmath.nat.infinitemath.rational.nnrat.identitiesmath.rational.signed.strict-ordermath.rational.signed.multiply-ordermath.rational.signed.equivalence-lawsmath.rational.nnrat.farkas-elim-list

nnrat/one-not-equivalent-zero :
  → proposition/negation (1 = 0)

signed/one-not-equivalent-zero :
  → proposition/negation (1 = 0)

signed/zero-less-than-one :
  → 0 < 1