Documentation

Apportionmentlib.Utils

Utils #

Utility functions and lemmas for Apportionmentlib.

source
def formatRat4 (r : ℚ) :
String

Formats a rational number to four decimal places.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem sum_pos_iff_exists_pos {n : ℕ} {v : Vector ℕ n} :
    0 < v.sum ↔ ∃ (i : Fin n), 0 < v[i]

    A vector of natural numbers has positive sum iff at least one component is positive.

    source
    theorem Vector.sum_four (v : Vector ℕ 4) :
    v.sum = v[0] + v[1] + v[2] + v[3]

    The sum of a length-4 vector equals the sum of its components.