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} [inst : One R] [inst : Zero R] [inst : Add R] :
R

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

Equations
class Nat.AtLeastTwo (n : ) :

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

Instances
    instance instOfNat {R : Type u_1} {n : } [inst : NatCast R] [inst : Nat.AtLeastTwo n] :
    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
    • instOfNat = { ofNat := n }
    @[simp]
    theorem Nat.cast_ofNat {R : Type u_1} {n : } [inst : NatCast R] [inst : Nat.AtLeastTwo n] :
    theorem Nat.cast_eq_ofNat {R : Type u_1} {n : } [inst : NatCast R] [inst : Nat.AtLeastTwo n] :
    n = OfNat.ofNat n

    Additive monoids with one #

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

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

    Instances
      class AddCommMonoidWithOne (R : Type u_1) extends AddMonoidWithOne :
      Type u_1
      • Addition is commutative in an additive commutative semigroup.

        add_comm : ∀ (a b : R), a + b = b + a

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

      Instances
        @[simp]
        theorem Nat.cast_zero {R : Type u_1} [inst : AddMonoidWithOne R] :
        0 = 0
        @[simp]
        theorem Nat.cast_succ {R : Type u_1} [inst : AddMonoidWithOne R] (n : ) :
        ↑(Nat.succ n) = n + 1
        theorem Nat.cast_add_one {R : Type u_1} [inst : AddMonoidWithOne R] (n : ) :
        ↑(n + 1) = n + 1
        @[simp]
        theorem Nat.cast_ite {R : Type u_1} [inst : AddMonoidWithOne R] (P : Prop) [inst : 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} [inst : AddMonoidWithOne R] :
        1 = 1
        @[simp]
        theorem Nat.cast_add {R : Type u_1} [inst : AddMonoidWithOne R] (m : ) (n : ) :
        ↑(m + n) = m + n
        def Nat.binCast {R : Type u_1} [inst : Zero R] [inst : One R] [inst : Add R] :
        R

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

        Equations
        @[simp]
        theorem Nat.binCast_eq {R : Type u_1} [inst : AddMonoidWithOne R] (n : ) :
        Nat.binCast n = n
        theorem Nat.cast_bit0 {R : Type u_1} [inst : AddMonoidWithOne R] (n : ) :
        ↑(bit0 n) = bit0 n
        theorem Nat.cast_bit1 {R : Type u_1} [inst : AddMonoidWithOne R] (n : ) :
        ↑(bit1 n) = bit1 n
        theorem Nat.cast_two {R : Type u_1} [inst : AddMonoidWithOne R] :
        2 = 2
        def AddMonoidWithOne.unary {R : Type u_1} [inst : AddMonoid R] [inst : One R] :

        AddMonoidWithOne implementation using unary recursion.

        Equations
        • AddMonoidWithOne.unary = let src := inst; let src_1 := inst; AddMonoidWithOne.mk
        def AddMonoidWithOne.binary {R : Type u_1} [inst : AddMonoid R] [inst : One R] :

        AddMonoidWithOne implementation using binary recursion.

        Equations
        • AddMonoidWithOne.binary = let src := inst; let src_1 := inst; AddMonoidWithOne.mk
        theorem NeZero.natCast_ne (n : ) (R : Type u_1) [inst : AddMonoidWithOne R] [h : NeZero n] :
        n 0
        theorem NeZero.of_neZero_natCast (R : Type u_1) [inst : AddMonoidWithOne R] {n : } [h : NeZero n] :
        theorem NeZero.pos_of_neZero_natCast (R : Type u_1) [inst : AddMonoidWithOne R] {n : } [inst : NeZero n] :
        0 < n
        theorem one_add_one_eq_two {α : Type u_1} [inst : AddMonoidWithOne α] :
        1 + 1 = 2
        theorem two_add_one_eq_three {α : Type u_1} [inst : AddMonoidWithOne α] :
        2 + 1 = 3
        theorem three_add_one_eq_four {α : Type u_1} [inst : AddMonoidWithOne α] :
        3 + 1 = 4