Documentation

Mathlib.Init.Data.Int.Basic

theorem Int.coe_nat_eq (n : ) :
n = Int.ofNat n
@[deprecated]

The number 0 : ℤ, as a standalone definition.

Equations
Instances For
    @[deprecated]

    The number 1 : ℤ, as a standalone definition.

    Equations
    Instances For
      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
      @[deprecated Int.natAbs_eq_zero]
      theorem Int.eq_zero_of_natAbs_eq_zero {a : } :
      Int.natAbs a = 0a = 0
      @[deprecated Int.natAbs_pos]
      theorem Int.natAbs_pos_of_ne_zero {a : } (h : a 0) :
      def Int.natMod (m : ) (n : ) :

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

      Equations
      Instances For