Reference · Non-negative rationals

rainbow.math.rational.nnrat.power

Non-negative rationalssrc/rainbow/math/rational/nnrat/power.clj1 definitions, 0 theorems

Exact powers of a nonnegative rational. `nnrat/power base steps` is the Nat recursor over multiplication from one, so `power base 0` reduces to one and `power base (succ n)` reduces to `base * power base n` definitionally -- consumers rewrite by reflexivity, no unfold lemmas needed. Built for the geometric decay of total variation along kernel iterates; generic and reusable anywhere an exact rational envelope is stated. Native on D63.

nnrat/power :
  (x₁ : ℚ≥0) (x₂ : ℕ)
  → ℚ≥0