Documentation

Mathlib.Init.Data.Int.Basic

theorem Int.ofNat_add_out (m : ) (n : ) :
m + n = (m + n)
theorem Int.ofNat_mul_out (m : ) (n : ) :
m * n = (m * n)
theorem Int.ofNat_add_one_out (n : ) :
n + 1 = n.succ
theorem Int.neg_eq_neg {a : } {b : } (h : -a = -b) :
a = b
def Int.natMod (m : ) (n : ) :

The modulus of an integer by another as a natural. Uses the E-rounding convention.

Equations
  • m.natMod n = (m % n).toNat
Instances For