Documentation

Mathlib.Data.Nat.Cast.Basic

Cast of natural numbers (additional theorems) #

This file proves additional properties about the canonical homomorphism from the natural numbers into an additive monoid with a one (Nat.cast).

Main declarations #

Nat.cast : ℕ → α as an AddMonoidHom.

Equations
    Instances For
      theorem Even.natCast {α : Type u_1} [AddMonoidWithOne α] {n : } (hn : Even n) :
      Even n
      @[simp]
      theorem Nat.cast_mul {α : Type u_1} [NonAssocSemiring α] (m n : ) :
      ↑(m * n) = m * n

      Nat.cast : ℕ → α as a RingHom

      Equations
        Instances For
          @[simp]
          theorem nsmul_eq_mul' {α : Type u_1} [NonAssocSemiring α] (a : α) (n : ) :
          n a = a * n
          @[simp]
          theorem nsmul_eq_mul {α : Type u_1} [NonAssocSemiring α] (n : ) (a : α) :
          n a = n * a
          @[simp]
          theorem Nat.cast_pow {α : Type u_1} [Semiring α] (m n : ) :
          ↑(m ^ n) = m ^ n
          theorem Nat.cast_dvd_cast {α : Type u_1} [Semiring α] {m n : } (h : m n) :
          m n
          theorem Dvd.dvd.natCast {α : Type u_1} [Semiring α] {m n : } (h : m n) :
          m n

          Alias of Nat.cast_dvd_cast.

          theorem eq_natCast' {A : Type u_3} {F : Type u_5} [FunLike F A] [AddMonoidWithOne A] [AddMonoidHomClass F A] (f : F) (h1 : f 1 = 1) (n : ) :
          f n = n
          theorem map_natCast' {B : Type u_4} {F : Type u_5} [AddMonoidWithOne B] {A : Type u_6} [AddMonoidWithOne A] [FunLike F A B] [AddMonoidHomClass F A B] (f : F) (h : f 1 = 1) (n : ) :
          f n = n
          theorem map_ofNat' {B : Type u_4} {F : Type u_5} [AddMonoidWithOne B] {A : Type u_6} [AddMonoidWithOne A] [FunLike F A B] [AddMonoidHomClass F A B] (f : F) (h : f 1 = 1) (n : ) [n.AtLeastTwo] :
          theorem ext_nat'' {A : Type u_3} {F : Type u_4} [MulZeroOneClass A] [FunLike F A] [ZeroHomClass F A] (f g : F) (h_pos : ∀ {n : }, 0 < nf n = g n) :
          f = g

          If two MonoidWithZeroHoms agree on the positive naturals they are equal.

          theorem MonoidWithZeroHom.ext_nat {A : Type u_3} [MulZeroOneClass A] {f g : →*₀ A} :
          (∀ {n : }, 0 < nf n = g n)f = g
          theorem MonoidWithZeroHom.ext_nat_iff {A : Type u_3} [MulZeroOneClass A] {f g : →*₀ A} :
          f = g ∀ {n : }, 0 < nf n = g n
          @[simp]
          theorem eq_natCast {R : Type u_3} {F : Type u_5} [NonAssocSemiring R] [FunLike F R] [RingHomClass F R] (f : F) (n : ) :
          f n = n
          @[simp]
          theorem map_natCast {R : Type u_3} {S : Type u_4} {F : Type u_5} [NonAssocSemiring R] [NonAssocSemiring S] [FunLike F R S] [RingHomClass F R S] (f : F) (n : ) :
          f n = n
          theorem map_ofNat {R : Type u_3} {S : Type u_4} {F : Type u_5} [NonAssocSemiring R] [NonAssocSemiring S] [FunLike F R S] [RingHomClass F R S] (f : F) (n : ) [n.AtLeastTwo] :

          This lemma is not marked @[simp] lemma because its #discr_tree_key (for the LHS) would just be DFunLike.coe _ _, due to the ofNat that https://github.com/leanprover/lean4/issues/2867 forces us to include, and therefore it would negatively impact performance.

          If that issue is resolved, this can be marked @[simp].

          theorem ext_nat {R : Type u_3} {F : Type u_5} [NonAssocSemiring R] [FunLike F R] [RingHomClass F R] (f g : F) :
          f = g
          theorem NeZero.nat_of_neZero {R : Type u_6} {S : Type u_7} [NonAssocSemiring R] [NonAssocSemiring S] {F : Type u_8} [FunLike F R S] [RingHomClass F R S] (f : F) {n : } [hn : NeZero n] :
          NeZero n

          This is primed to match eq_intCast'.

          @[simp]
          theorem Nat.cast_id (n : ) :
          n = n

          We don't use RingHomClass here, since that might cause type-class slowdown for Subsingleton.

          Equations
            instance Pi.instNatCast {α : Type u_1} {π : αType u_3} [(a : α) → NatCast (π a)] :
            NatCast ((a : α) → π a)
            Equations
              @[simp]
              theorem Pi.natCast_apply {α : Type u_1} {π : αType u_3} [(a : α) → NatCast (π a)] (n : ) (a : α) :
              n a = n
              theorem Pi.natCast_def {α : Type u_1} {π : αType u_3} [(a : α) → NatCast (π a)] (n : ) :
              n = fun (x : α) => n
              @[instance 100]
              instance Pi.instOfNat {α : Type u_1} {π : αType u_3} (n : ) [(i : α) → OfNat (π i) n] :
              OfNat ((i : α) → π i) n
              Equations
                @[simp]
                theorem Pi.ofNat_apply {α : Type u_1} {π : αType u_3} (n : ) [(i : α) → OfNat (π i) n] (a : α) :
                theorem Pi.ofNat_def {α : Type u_1} {π : αType u_3} (n : ) [(i : α) → OfNat (π i) n] :
                OfNat.ofNat n = fun (x : α) => OfNat.ofNat n
                theorem Sum.elim_natCast_natCast {α : Type u_3} {β : Type u_4} {γ : Type u_5} [NatCast γ] (n : ) :
                Sum.elim n n = n