Reference · Non-negative rationals

rainbow.math.rational.nnrat.identities

Neutral and absorbing laws for native nonnegative rationals, up to cross-product equivalence.

nnrat/add-zero-right

TheoremFor all inputsNo axiomsSource, line 95

nnrat/add-zero-right :
  (value : ℚ≥0)
  → value + 0 = value

+ = nnrat/add0 = nnrat/zero= = nnrat/equivalent: equality of rational valuesℚ≥0 = nnrat/NonnegativeRational

TheoremFor all inputsNo axiomsSource, line 136

nnrat/add-zero-left :
  (value : ℚ≥0)
  → 0 + value = value

+ = nnrat/add0 = nnrat/zero= = nnrat/equivalent: equality of rational valuesℚ≥0 = nnrat/NonnegativeRational

TheoremFor all inputsNo axiomsSource, line 183

nnrat/multiply-one-right :
  (value : ℚ≥0)
  → value · 1 = value

1 = nnrat/one= = nnrat/equivalent: equality of rational values· = nnrat/multiplyℚ≥0 = nnrat/NonnegativeRational

TheoremFor all inputsNo axiomsSource, line 216

nnrat/multiply-one-left :
  (x : ℚ≥0)
  → 1 · x = x

1 = nnrat/one= = nnrat/equivalent: equality of rational values· = nnrat/multiplyℚ≥0 = nnrat/NonnegativeRational

TheoremFor all inputsNo axiomsSource, line 249

nnrat/multiply-zero-right :
  (value : ℚ≥0)
  → value · 0 = 0

0 = nnrat/zero= = nnrat/equivalent: equality of rational values· = nnrat/multiplyℚ≥0 = nnrat/NonnegativeRational

TheoremFor all inputsNo axiomsSource, line 271

nnrat/multiply-zero-left :
  (value : ℚ≥0)
  → 0 · value = 0

0 = nnrat/zero= = nnrat/equivalent: equality of rational values· = nnrat/multiplyℚ≥0 = nnrat/NonnegativeRational

TheoremWorked exampleNo axiomsSource, line 292

nnrat/reciprocal-one :
  → nnrat/reciprocal 1 = 1

1 = nnrat/one= = nnrat/equivalent: equality of rational values

TheoremFor all inputsNo axiomsSource, line 300

nnrat/divide-one-right :
  (value : ℚ≥0)
  → nnrat/divide value 1 = value

1 = nnrat/one= = nnrat/equivalent: equality of rational valuesℚ≥0 = nnrat/NonnegativeRational