Documentation

Init.Data.Nat.Div

theorem Nat.div_rec_lemma {x : Nat} {y : Nat} :
0 < y y xx - y < x
@[extern lean_nat_div]
def Nat.div (x : Nat) (y : Nat) :
Equations
Instances For
    theorem Nat.div_eq (x : Nat) (y : Nat) :
    x / y = if 0 < y y x then (x - y) / y + 1 else 0
    theorem Nat.div.inductionOn {motive : NatNatSort u} (x : Nat) (y : Nat) (ind : (x y : Nat) → 0 < y y xmotive (x - y) ymotive x y) (base : (x y : Nat) → ¬(0 < y y x)motive x y) :
    motive x y
    theorem Nat.div_le_self (n : Nat) (k : Nat) :
    n / k n
    theorem Nat.div_lt_self {n : Nat} {k : Nat} (hLtN : 0 < n) (hLtK : 1 < k) :
    n / k < n
    @[extern lean_nat_mod]
    def Nat.modCore (x : Nat) (y : Nat) :
    Equations
    Instances For
      @[extern lean_nat_mod]
      def Nat.mod :
      NatNatNat
      Instances For
        theorem Nat.modCore_eq_mod (x : Nat) (y : Nat) :
        Nat.modCore x y = x % y
        theorem Nat.mod_eq (x : Nat) (y : Nat) :
        x % y = if 0 < y y x then (x - y) % y else x
        theorem Nat.mod.inductionOn {motive : NatNatSort u} (x : Nat) (y : Nat) (ind : (x y : Nat) → 0 < y y xmotive (x - y) ymotive x y) (base : (x y : Nat) → ¬(0 < y y x)motive x y) :
        motive x y
        @[simp]
        theorem Nat.mod_zero (a : Nat) :
        a % 0 = a
        theorem Nat.mod_eq_of_lt {a : Nat} {b : Nat} (h : a < b) :
        a % b = a
        theorem Nat.mod_eq_sub_mod {a : Nat} {b : Nat} (h : a b) :
        a % b = (a - b) % b
        theorem Nat.mod_lt (x : Nat) {y : Nat} :
        y > 0x % y < y
        theorem Nat.mod_le (x : Nat) (y : Nat) :
        x % y x
        @[simp]
        theorem Nat.zero_mod (b : Nat) :
        0 % b = 0
        @[simp]
        theorem Nat.mod_self (n : Nat) :
        n % n = 0
        theorem Nat.mod_one (x : Nat) :
        x % 1 = 0
        theorem Nat.div_add_mod (m : Nat) (n : Nat) :
        n * (m / n) + m % n = m