Documentation

Mathlib.Data.Nat.Cast.Defs

Cast of natural numbers #

This file defines the canonical homomorphism from the natural numbers into an AddMonoid with a one. In additive monoids with one, there exists a unique such homomorphism and we store it in the natCast : ℕ → R field.

Preferentially, the homomorphism is written as the coercion Nat.cast.

Main declarations #

def Nat.unaryCast {R : Type u_1} [One R] [Zero R] [Add R] :
R

The numeral ((0+1)+⋯)+1.

Equations
Instances For
    class Nat.AtLeastTwo (n : ) :

    A type class for natural numbers which are greater than or equal to 2.

    Instances
      theorem Nat.AtLeastTwo.prop {n : } [self : n.AtLeastTwo] :
      n 2
      instance instNatAtLeastTwo {n : } :
      (n + 2).AtLeastTwo
      Equations
      • =
      theorem Nat.AtLeastTwo.one_lt {n : } [n.AtLeastTwo] :
      1 < n
      theorem Nat.AtLeastTwo.ne_one {n : } [n.AtLeastTwo] :
      n 1
      @[instance 100]
      instance instOfNatAtLeastTwo {R : Type u_1} {n : } [NatCast R] [n.AtLeastTwo] :
      OfNat R n

      Recognize numeric literals which are at least 2 as terms of R via Nat.cast. This instance is what makes things like 37 : R type check. Note that 0 and 1 are not needed because they are recognized as terms of R (at least when R is an AddMonoidWithOne) through Zero and One, respectively.

      Equations
      • instOfNatAtLeastTwo = { ofNat := n }
      @[simp]
      theorem Nat.cast_ofNat {R : Type u_1} {n : } [NatCast R] [n.AtLeastTwo] :
      theorem Nat.cast_eq_ofNat {R : Type u_1} {n : } [NatCast R] [n.AtLeastTwo] :
      n = OfNat.ofNat n

      Additive monoids with one #

      class AddMonoidWithOne (R : Type u_2) extends NatCast , AddMonoid , One :
      Type u_2

      An AddMonoidWithOne is an AddMonoid with a 1. It also contains data for the unique homomorphism ℕ → R.

      Instances

        The canonical map ℕ → R sends 0 : ℕ to 0 : R.

        The canonical map ℕ → R is a homomorphism.

        class AddCommMonoidWithOne (R : Type u_2) extends AddMonoidWithOne :
        Type u_2

        An AddCommMonoidWithOne is an AddMonoidWithOne satisfying a + b = b + a.

        Instances
          @[simp]
          theorem Nat.cast_zero {R : Type u_1} [AddMonoidWithOne R] :
          0 = 0
          theorem Nat.cast_succ {R : Type u_1} [AddMonoidWithOne R] (n : ) :
          n.succ = n + 1
          theorem Nat.cast_add_one {R : Type u_1} [AddMonoidWithOne R] (n : ) :
          (n + 1) = n + 1
          @[simp]
          theorem Nat.cast_ite {R : Type u_1} [AddMonoidWithOne R] (P : Prop) [Decidable P] (m : ) (n : ) :
          (if P then m else n) = if P then m else n
          @[simp]
          theorem Nat.cast_one {R : Type u_1} [AddMonoidWithOne R] :
          1 = 1
          @[simp]
          theorem Nat.cast_add {R : Type u_1} [AddMonoidWithOne R] (m : ) (n : ) :
          (m + n) = m + n
          @[irreducible]
          def Nat.binCast {R : Type u_1} [Zero R] [One R] [Add R] :
          R

          Computationally friendlier cast than Nat.unaryCast, using binary representation.

          Equations
          • Nat.binCast 0 = 0
          • n.succ.binCast = if (n + 1) % 2 = 0 then ((n + 1) / 2).binCast + ((n + 1) / 2).binCast else ((n + 1) / 2).binCast + ((n + 1) / 2).binCast + 1
          Instances For
            @[simp]
            theorem Nat.binCast_eq {R : Type u_1} [AddMonoidWithOne R] (n : ) :
            n.binCast = n
            @[deprecated]
            theorem Nat.cast_bit0 {R : Type u_1} [AddMonoidWithOne R] (n : ) :
            (bit0 n) = bit0 n
            @[deprecated]
            theorem Nat.cast_bit1 {R : Type u_1} [AddMonoidWithOne R] (n : ) :
            (bit1 n) = bit1 n
            theorem Nat.cast_two {R : Type u_1} [AddMonoidWithOne R] :
            2 = 2
            @[reducible, inline]

            AddMonoidWithOne implementation using unary recursion.

            Equations
            Instances For
              @[reducible, inline]

              AddMonoidWithOne implementation using binary recursion.

              Equations
              Instances For
                theorem one_add_one_eq_two {R : Type u_1} [AddMonoidWithOne R] :
                1 + 1 = 2
                theorem two_add_one_eq_three {R : Type u_1} [AddMonoidWithOne R] :
                2 + 1 = 3
                theorem three_add_one_eq_four {R : Type u_1} [AddMonoidWithOne R] :
                3 + 1 = 4