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
    @[simp]
    theorem Nat.coe_castAddMonoidHom {α : Type u_1} [AddMonoidWithOne α] :
    (Nat.castAddMonoidHom α) = Nat.cast
    @[simp]
    theorem Nat.cast_mul {α : Type u_1} [NonAssocSemiring α] (m : ) (n : ) :
    (m * n) = m * n

    Nat.cast : ℕ → α as a RingHom

    Equations
    • Nat.castRingHom α = let __src := Nat.castAddMonoidHom α; { toMonoidHom := { toOneHom := { toFun := Nat.cast, map_one' := }, map_mul' := }, map_zero' := , map_add' := }
    Instances For
      @[simp]
      theorem Nat.coe_castRingHom {α : Type u_1} [NonAssocSemiring α] :
      (Nat.castRingHom α) = Nat.cast
      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.coe_nat_dvd {α : 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.coe_nat_dvd.

      theorem ext_nat' {A : Type u_3} {F : Type u_5} [FunLike F A] [AddMonoid A] [AddMonoidHomClass F A] (f : F) (g : F) (h : f 1 = g 1) :
      f = g
      theorem AddMonoidHom.ext_nat {A : Type u_3} [AddMonoid A] {f : →+ A} {g : →+ A} :
      f 1 = g 1f = g
      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 : ) [Nat.AtLeastTwo n] :
      @[simp]
      theorem nsmul_one {A : Type u_6} [AddMonoidWithOne A] (n : ) :
      n 1 = n
      theorem ext_nat'' {A : Type u_3} {F : Type u_4} [MulZeroOneClass A] [FunLike F A] [MonoidWithZeroHomClass F A] (f : 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 : →*₀ A} {g : →*₀ A} :
      (∀ {n : }, 0 < nf n = g n)f = g
      @[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
      @[simp]
      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 : ) [Nat.AtLeastTwo n] :
      theorem ext_nat {R : Type u_3} {F : Type u_5} [NonAssocSemiring R] [FunLike F R] [RingHomClass F R] (f : F) (g : F) :
      f = g
      theorem NeZero.nat_of_neZero {R : Type u_6} {S : Type u_7} [Semiring R] [Semiring 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
      • Nat.uniqueRingHom = { toInhabited := { default := Nat.castRingHom R }, uniq := }
      def multiplesHom (α : Type u_1) [AddMonoid α] :
      α ( →+ α)

      Additive homomorphisms from are defined by the image of 1.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        def powersHom (α : Type u_1) [Monoid α] :

        Monoid homomorphisms from Multiplicative are defined by the image of Multiplicative.ofAdd 1.

        Equations
        Instances For
          @[simp]
          theorem multiplesHom_apply {α : Type u_1} [AddMonoid α] (x : α) (n : ) :
          ((multiplesHom α) x) n = n x
          @[simp]
          theorem powersHom_apply {α : Type u_1} [Monoid α] (x : α) (n : Multiplicative ) :
          ((powersHom α) x) n = x ^ Multiplicative.toAdd n
          @[simp]
          theorem multiplesHom_symm_apply {α : Type u_1} [AddMonoid α] (f : →+ α) :
          (multiplesHom α).symm f = f 1
          @[simp]
          theorem powersHom_symm_apply {α : Type u_1} [Monoid α] (f : Multiplicative →* α) :
          (powersHom α).symm f = f (Multiplicative.ofAdd 1)
          theorem MonoidHom.apply_mnat {α : Type u_1} [Monoid α] (f : Multiplicative →* α) (n : Multiplicative ) :
          f n = f (Multiplicative.ofAdd 1) ^ Multiplicative.toAdd n
          theorem MonoidHom.ext_mnat {α : Type u_1} [Monoid α] ⦃f : Multiplicative →* α ⦃g : Multiplicative →* α (h : f (Multiplicative.ofAdd 1) = g (Multiplicative.ofAdd 1)) :
          f = g
          theorem AddMonoidHom.apply_nat {α : Type u_1} [AddMonoid α] (f : →+ α) (n : ) :
          f n = n f 1
          def multiplesAddHom (α : Type u_1) [AddCommMonoid α] :
          α ≃+ ( →+ α)

          If α is commutative, multiplesHom is an additive equivalence.

          Equations
          Instances For
            def powersMulHom (α : Type u_1) [CommMonoid α] :

            If α is commutative, powersHom is a multiplicative equivalence.

            Equations
            Instances For
              @[simp]
              theorem multiplesAddHom_apply (α : Type u_1) [AddCommMonoid α] (x : α) (n : ) :
              ((multiplesAddHom α) x) n = n x
              @[simp]
              theorem powersMulHom_apply (α : Type u_1) [CommMonoid α] (x : α) (n : Multiplicative ) :
              ((powersMulHom α) x) n = x ^ Multiplicative.toAdd n
              @[simp]
              theorem multiplesAddHom_symm_apply (α : Type u_1) [AddCommMonoid α] (f : →+ α) :
              @[simp]
              theorem powersMulHom_symm_apply (α : Type u_1) [CommMonoid α] (f : Multiplicative →* α) :
              (MulEquiv.symm (powersMulHom α)) f = f (Multiplicative.ofAdd 1)
              instance Pi.natCast {α : Type u_1} {π : αType u_3} [(a : α) → NatCast (π a)] :
              NatCast ((a : α) → π a)
              Equations
              • Pi.natCast = { natCast := fun (n : ) (x : α) => n }
              theorem Pi.nat_apply {α : Type u_1} {π : αType u_3} [(a : α) → NatCast (π a)] (n : ) (a : α) :
              n a = n
              @[simp]
              theorem Pi.coe_nat {α : Type u_1} {π : αType u_3} [(a : α) → NatCast (π a)] (n : ) :
              n = fun (x : α) => n
              @[simp]
              theorem Pi.ofNat_apply {α : Type u_1} {π : αType u_3} [(a : α) → NatCast (π a)] (n : ) [Nat.AtLeastTwo n] (a : α) :
              OfNat.ofNat n a = n
              theorem Sum.elim_natCast_natCast {α : Type u_3} {β : Type u_4} {γ : Type u_5} [NatCast γ] (n : ) :
              Sum.elim n n = n