bend-collections-laws-math

Releases (1)

• 1.0.0.0 indexed

Definitions (5,526)

proofs/math/natural/arith.bend

• def mod_mod(x mod n) mod n == x mod n (Mathlib Nat.mod_mod)
• def mod_add_r(x + y mod n) mod n == (x + y) mod n (Mathlib Nat.add_mod)
• def mod_add_l
• def mod_mul_r(x (y mod n)) mod n == (x y) mod n (Mathlib Nat.mul_mod)
• def mod_mul_l
• def pow_adda^(x + y) == a^x a^y (Mathlib pow_add)
• def mul_swap4(a b)(c d) == (a c)(b d)
• def mul_pow(x y)^k == x^k y^k (Mathlib mul_pow)

proofs/math/natural/bits.bend

• def half_eqn == 2 (n / 2) + n mod 2
• def add_succ_nlea + (1 + b) <= a is false
• def half_ltn / 2 < n for n > 0
• def half_remn mod 2 <= 1
• def go_acc
• def go_zero
• def half_fuelthe halved argument stays within the fuel
• def half_bound2 h + r < 2 (1 + h) for r < 2
• def lt_go
• def bit_length_ltn < 2^bit_length(n) (Mathlib Nat.lt_size_self)
• def le_stepthe lower bound, as 2^L <= max(1, 2 n)
• def le_go
• def bit_length_le2^bit_length(n) <= 2 n for n > 0, i.e.
• def bit_length_zero

proofs/math/natural/fact.bend

• def mul_left_comm(x a) f == a (x f)
• def factorial_go
• def factorial_okfactorial(n) == n!
• def pos_mul
• def factorial_pos0 < n!
• def desc_succ(1+m).desc(1+j) == (1+m) * m.desc(j) (Mathlib Nat.succ_descFactorial_succ)
• def desc_frontm * (m - 1).desc(j) == m.desc(1+j), the order perm multiplies in
• def perm_go
• def perm_okperm(n, k) == n.descFactorial(k)
• def desc_selfn.desc(n) == n!
• def sub_lt_succj < n gives n - j == 1 + (n - (1 + j))
• def factorial_mul_desc(n - k)!
• def choose_zero_right
• def choose_one_rightC(n, 1) == n
• def succ_mul_choose(n + 1) C(n, k) == C(n + 1, k + 1) (k + 1) (Mathlib Nat.add_one_mul_choose_eq)
• def mul_sub_lefta (x - y) == a x - a y
• def choose_succ_rightC(n, k + 1) (k + 1) == C(n, k) (n - k) (Mathlib Nat.choose_succ_right_eq)
• def choose_mul_factorialC(n, k) k!
• def choose_eq_zeron < k gives C(n, k) == 0 (Mathlib Nat.choose_eq_zero_of_lt)
• def pos_pos
• def choose_mul_factsC(n, k) (k!
• def sub_sub_selfn - (n - k) == k for k <= n
• def sub_le_self
• def choose_symmC(n, n - k) == C(n, k) (Mathlib Nat.choose_symm)
• def comb_goevery r_i is C(n, i), so each division is exact
• def comb_min
• def comb_small
• def comb_okcomb(n, k) == C(n, k)

proofs/math/natural/gcd.bend

• def dvd_modd | a and d | n give d | a mod n: a mod n == (ka - q kn) d, q = a / n
• def dvd_of_modd | n and d | a mod n give d | a: a == (q kn + kr) d
• type Witthe quotients a / g and b / g, by Euclid's recursion
• def wl
• def wr
• def wstepfrom n == l g and a mod n == r g: a == (q l + r) g and n == l g
• def ws
• def divides_both
• def step_both
• def gcd_both
• def dwthe quotient g / d, for d | a (a == ka d) and d | b (b == kb d)
• def gcd_greatest
• def both_l
• def both_r
• def gcd_dvd_left
• def gcd_dvd_right
• def dvd_gcd

proofs/math/natural/inverse.bend

• def bg
• def bc
• def cong_add_r
• def cong_mul_r
• def shift(z + c) + k == M + z when c + k == M
• def add_cancel_modx + c == y + c (mod m) gives x == y (mod m): add m - (c mod m) to both
• def sub_plusu + t == m for t < m, u = m - t
• def inv_step_okone extended-Euclid step keeps the invariant
• def inv_inv
• def inv_rthe remainders are Euclid's
• def unwrap
• def is_done
• def mod_self
• def inv_bzthe extended-Euclid state mod_inverse(a, m) ends in
• def inv_bezout
• def inv_kmthe final remainder divides m and a
• def inv_ka
• def inv_dvd_m
• def inv_dvd_a2
• def inv_dvd_a
• def done_bz
• def inverse_donemod_inverse(a, m) == Done{x}: a x == 1 (mod m) and x < m (Mathlib ZMod.mul_inv_of_unit)
• def fail_bz
• def inverse_failmod_inverse(a, m) == Fail{NotInvertible}: g >= 2 divides a and m, so a and m are not coprime (Mathlib Nat.Coprime, ZMod.unitOfCoprime)
• def inverse_zero

proofs/math/natural/lcm.bend

• def add_succ_zero
• def one_s
• def mul_eq_onea b == 1 gives a == 1 (Mathlib Nat.eq_one_of_mul_eq_one_right)
• def one_mul
• def dvd_antisymmx == kx y and y == ky x give x == y (Mathlib Nat.dvd_antisymm)
• def swap_cwc (w g) == w (c g)
• def scale_dvdx == w g gives c x == w (c g)
• def unscalec x == w (h c) gives x == w h (c > 0)