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
        instance instNatAtLeastTwo {n : } :
        @[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
          @[simp]
          theorem Nat.cast_ofNat {R : Type u_1} {n : } [NatCast R] [n.AtLeastTwo] :
          @[deprecated Nat.cast_ofNat (since := "2024-12-22")]
          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 R, AddMonoid R, One R :
          Type u_2

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

          Instances
            class AddCommMonoidWithOne (R : Type u_2) extends AddMonoidWithOne R, AddCommMonoid R :
            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
                Instances For
                  @[simp]
                  theorem Nat.binCast_eq {R : Type u_1} [AddMonoidWithOne R] (n : ) :
                  n.binCast = n
                  theorem Nat.cast_two {R : Type u_1} [NatCast R] :
                  2 = 2
                  theorem Nat.cast_three {R : Type u_1} [NatCast R] :
                  3 = 3
                  theorem Nat.cast_four {R : Type u_1} [NatCast R] :
                  4 = 4
                  @[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
                          theorem two_add_two_eq_four {R : Type u_1} [AddMonoidWithOne R] :
                          2 + 2 = 4
                          @[simp]
                          theorem nsmul_one {A : Type u_2} [AddMonoidWithOne A] (n : ) :
                          n 1 = n