bend-collections-laws-math

Search uses release 1.0.0.0 · 5,526 definitions

Releases (1)

def gcd_mul_pos
def gcd_mul_leftgcd(c a, c b) == c gcd(a, b) (Mathlib Nat.gcd_mul_left)
def gcd_posa == la g with a > 0 makes g positive
def div_exact
def lcm_pos
def lcm_wllcm(a, b) == kl a and lcm(a, b) == kr b (Mathlib Nat.dvd_lcm_left/right)
def lcm_wr
def dvd_lcm_left
def dvd_lcm_right
def gcd_mul_lcmgcd(a, b) lcm(a, b) == a b (Mathlib Nat.gcd_mul_lcm)
def cancel_pos
def lcm_dwthe quotient m / lcm(a, b) for a common multiple m == x a == y b
def lcm_dvd_pos
def lcm_dvdevery common multiple of a and b is a multiple of lcm(a, b) (Mathlib Nat.lcm_dvd)

def sum_go
def sum_ok
def prod_go
def prod_ok
def nth0
def dvd_withd divides every element: xs[i] == ks[i] d
def mul_withm is a multiple of every element: m == ks[i] xs[i]
def dvd_trans(a == k1 b and b == k2 c) gives a == (k1 k2) c
def gw_accthe quotient acc / gcd_all_go(xs, acc)
def g_acc
def gw_nththe quotient (xs[i]) / gcd_all_go(xs, acc)
def g_nth
def gcd_all_dvdgcd_all(xs) divides every element: xs[i] == k gcd_all(xs) (0 past the end) (Mathlib Finset.gcd_dvd)
def gw_dvdthe quotient gcd_all_go(xs, acc) / d for a common divisor d
def g_dvd
def dvd_gcd_allevery common divisor of the elements divides gcd_all(xs) (Mathlib Finset.dvd_gcd)
def lw_acc
def l_acc
def lw_nth
def l_nth
def dvd_lcm_allevery element divides lcm_all(xs) (1 past the end) (Mathlib Finset.dvd_lcm)
def lw_mul
def l_mul
def lcm_all_dvdlcm_all(xs) divides every common multiple of the elements (Mathlib Finset.lcm_dvd)

def le_add_ra <= b gives a + c <= b + c
def lt_add_posa < a + c for c > 0
def pow_gtk < b^k for b >= 2
def ilog_stopthe loop stops at k: b^k == p <= n < p b
def ilog_absurdwith no fuel left k == n, and p b <= n is impossible: n == k < p <= p b
def ilog_okthe loop: p == b^k <= n, up is p b <= n, fuel + k == n
def lt_two
def ilog_valuethe value ilog(n, b) returns for n >= 1, b >= 2
def ilog_done
def ilog_bounds
def fst_bb^ilog(n, b) <= n (Mathlib Nat.pow_log_le_self)
def snd_b
def pow_ilog_le
def lt_pow_succ_ilogn < b^(ilog(n, b) + 1) (Mathlib Nat.lt_pow_succ_log_self)
def ilog_zero
def or_true
def ilog_small_base

def mod_pow(x mod m)^k == x^k (mod m) (Mathlib Nat.pow_mod)
def pow_doublex^(2 y) == (x x)^y
def same_sqthe squared base, reduced, is x^(2 e2) under any factor c
def pm_bitone step: the odd bit multiplies acc by base
def odd_lt
def pm_gothe loop: acc < m, e <= fuel give pow_mod_go == acc base^e mod m
def pow_mod_okpow_mod(b, e, m) == Done{b^e mod m} (Mathlib Nat.pow_mod; Python pow(b, e, m))
def pow_mod_zero