Documentation

Mathlib.Init.Data.Int.Basic

The number 0 : ℤ, as a standalone definition.

Equations

The number 1 : ℤ, as a standalone definition.

Equations
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 = ↑(Nat.succ n)
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