Documentation

Init.Data.Nat.Mod

Further results about mod. #

This file proves some results about mod that are useful for bitblasting, in particular Nat.mod_mul : x % (a * b) = x % a + a * (x / a % b) and its corollary Nat.mod_pow_succ : x % b ^ (k + 1) = x % b ^ k + b ^ k * ((x / b ^ k) % b).

It contains the necessary preliminary results relating order and * and /, which should probably be moved to their own file.

@[simp]
theorem Nat.mul_lt_mul_left {a : Nat} {b : Nat} {c : Nat} (a0 : 0 < a) :
a * b < a * c b < c
@[simp]
theorem Nat.mul_lt_mul_right {a : Nat} {b : Nat} {c : Nat} (a0 : 0 < a) :
b * a < c * a b < c
theorem Nat.lt_of_mul_lt_mul_left {a : Nat} {b : Nat} {c : Nat} (h : a * b < a * c) :
b < c
theorem Nat.lt_of_mul_lt_mul_right {a : Nat} {b : Nat} {c : Nat} (h : b * a < c * a) :
b < c
theorem Nat.div_lt_of_lt_mul {m : Nat} {n : Nat} {k : Nat} (h : m < n * k) :
m / n < k
theorem Nat.mod_mul_right_div_self (m : Nat) (n : Nat) (k : Nat) :
m % (n * k) / n = m / n % k
theorem Nat.mod_mul_left_div_self (m : Nat) (n : Nat) (k : Nat) :
m % (k * n) / n = m / n % k
@[simp]
theorem Nat.mod_mul_right_mod (a : Nat) (b : Nat) (c : Nat) :
a % (b * c) % b = a % b
@[simp]
theorem Nat.mod_mul_left_mod (a : Nat) (b : Nat) (c : Nat) :
a % (b * c) % c = a % c
theorem Nat.mod_mul {a : Nat} {b : Nat} {x : Nat} :
x % (a * b) = x % a + a * (x / a % b)
theorem Nat.mod_pow_succ {x : Nat} {b : Nat} {k : Nat} :
x % b ^ (k + 1) = x % b ^ k + b ^ k * (x / b ^ k % b)
@[simp]
theorem Nat.two_pow_mod_two_eq_zero {n : Nat} :
2 ^ n % 2 = 0 0 < n
@[simp]
theorem Nat.two_pow_mod_two_eq_one {n : Nat} :
2 ^ n % 2 = 1 n = 0