Documentation

Mathlib.Data.Int.Cast.Lemmas

Cast of integers (additional theorems) #

This file proves additional properties about the canonical homomorphism from the integers into an additive group with a one (Int.cast), particularly results involving algebraic homomorphisms or the order structure on which were not available in the import dependencies of Data.Int.Cast.Basic.

Main declarations #

Coercion ℕ → ℤ as a RingHom.

Equations
Instances For
    @[simp]
    theorem Int.cast_ite {α : Type u_3} [AddGroupWithOne α] (P : Prop) [Decidable P] (m : ) (n : ) :
    (if P then m else n) = if P then m else n
    def Int.castAddHom (α : Type u_5) [AddGroupWithOne α] :

    coe : ℤ → α as an AddMonoidHom.

    Equations
    • Int.castAddHom α = { toFun := Int.cast, map_zero' := , map_add' := }
    Instances For
      @[simp]
      theorem Int.coe_castAddHom {α : Type u_3} [AddGroupWithOne α] :
      (Int.castAddHom α) = fun (x : ) => x
      theorem Even.intCast {α : Type u_3} [AddGroupWithOne α] {n : } (h : Even n) :
      Even n
      @[simp]
      theorem Int.cast_eq_zero {α : Type u_3} [AddGroupWithOne α] [CharZero α] {n : } :
      n = 0 n = 0
      @[simp]
      theorem Int.cast_inj {α : Type u_3} [AddGroupWithOne α] [CharZero α] {m : } {n : } :
      m = n m = n
      theorem Int.cast_ne_zero {α : Type u_3} [AddGroupWithOne α] [CharZero α] {n : } :
      n 0 n 0
      @[simp]
      theorem Int.cast_eq_one {α : Type u_3} [AddGroupWithOne α] [CharZero α] {n : } :
      n = 1 n = 1
      theorem Int.cast_ne_one {α : Type u_3} [AddGroupWithOne α] [CharZero α] {n : } :
      n 1 n 1
      def Int.castRingHom (α : Type u_3) [NonAssocRing α] :

      coe : ℤ → α as a RingHom.

      Equations
      • Int.castRingHom α = { toFun := Int.cast, map_one' := , map_mul' := , map_zero' := , map_add' := }
      Instances For
        @[simp]
        theorem Int.coe_castRingHom {α : Type u_3} [NonAssocRing α] :
        (Int.castRingHom α) = fun (x : ) => x
        theorem Int.cast_commute {α : Type u_3} [NonAssocRing α] (n : ) (a : α) :
        Commute (↑n) a
        theorem Int.cast_comm {α : Type u_3} [NonAssocRing α] (n : ) (x : α) :
        n * x = x * n
        theorem Int.commute_cast {α : Type u_3} [NonAssocRing α] (a : α) (n : ) :
        Commute a n
        @[simp]
        theorem zsmul_eq_mul {α : Type u_3} [NonAssocRing α] (a : α) (n : ) :
        n a = n * a
        theorem zsmul_eq_mul' {α : Type u_3} [NonAssocRing α] (a : α) (n : ) :
        n a = a * n
        theorem Odd.intCast {α : Type u_3} [Ring α] {n : } (hn : Odd n) :
        Odd n
        theorem Int.cast_dvd_cast {α : Type u_3} [CommRing α] (m : ) (n : ) (h : m n) :
        m n
        @[deprecated Int.cast_dvd_cast]
        theorem Int.coe_int_dvd {α : Type u_3} [CommRing α] (m : ) (n : ) (h : m n) :
        m n

        Alias of Int.cast_dvd_cast.

        @[simp]
        theorem SemiconjBy.intCast_mul_right {α : Type u_3} [Ring α] {a : α} {x : α} {y : α} (h : SemiconjBy a x y) (n : ) :
        SemiconjBy a (n * x) (n * y)
        @[simp]
        theorem SemiconjBy.intCast_mul_left {α : Type u_3} [Ring α] {a : α} {x : α} {y : α} (h : SemiconjBy a x y) (n : ) :
        SemiconjBy (n * a) x y
        @[simp]
        theorem SemiconjBy.intCast_mul_intCast_mul {α : Type u_3} [Ring α] {a : α} {x : α} {y : α} (h : SemiconjBy a x y) (m : ) (n : ) :
        SemiconjBy (m * a) (n * x) (n * y)
        @[deprecated SemiconjBy.intCast_mul_right]
        theorem SemiconjBy.cast_int_mul_right {α : Type u_3} [Ring α] {a : α} {x : α} {y : α} (h : SemiconjBy a x y) (n : ) :
        SemiconjBy a (n * x) (n * y)

        Alias of SemiconjBy.intCast_mul_right.

        @[deprecated SemiconjBy.intCast_mul_left]
        theorem SemiconjBy.cast_int_mul_left {α : Type u_3} [Ring α] {a : α} {x : α} {y : α} (h : SemiconjBy a x y) (n : ) :
        SemiconjBy (n * a) x y

        Alias of SemiconjBy.intCast_mul_left.

        @[deprecated SemiconjBy.intCast_mul_intCast_mul]
        theorem SemiconjBy.cast_int_mul_cast_int_mul {α : Type u_3} [Ring α] {a : α} {x : α} {y : α} (h : SemiconjBy a x y) (m : ) (n : ) :
        SemiconjBy (m * a) (n * x) (n * y)

        Alias of SemiconjBy.intCast_mul_intCast_mul.

        @[simp]
        theorem Commute.intCast_left {α : Type u_3} [NonAssocRing α] {a : α} {n : } :
        Commute (↑n) a
        @[simp]
        theorem Commute.intCast_right {α : Type u_3} [NonAssocRing α] {a : α} {n : } :
        Commute a n
        @[deprecated Commute.intCast_right]
        theorem Commute.cast_int_right {α : Type u_3} [NonAssocRing α] {a : α} {n : } :
        Commute a n

        Alias of Commute.intCast_right.

        @[deprecated Commute.intCast_left]
        theorem Commute.cast_int_left {α : Type u_3} [NonAssocRing α] {a : α} {n : } :
        Commute (↑n) a

        Alias of Commute.intCast_left.

        @[simp]
        theorem Commute.intCast_mul_right {α : Type u_3} [Ring α] {a : α} {b : α} (h : Commute a b) (m : ) :
        Commute a (m * b)
        @[simp]
        theorem Commute.intCast_mul_left {α : Type u_3} [Ring α] {a : α} {b : α} (h : Commute a b) (m : ) :
        Commute (m * a) b
        theorem Commute.intCast_mul_intCast_mul {α : Type u_3} [Ring α] {a : α} {b : α} (h : Commute a b) (m : ) (n : ) :
        Commute (m * a) (n * b)
        theorem Commute.self_intCast_mul {α : Type u_3} [Ring α] (a : α) (n : ) :
        Commute a (n * a)
        theorem Commute.intCast_mul_self {α : Type u_3} [Ring α] (a : α) (n : ) :
        Commute (n * a) a
        theorem Commute.self_intCast_mul_intCast_mul {α : Type u_3} [Ring α] (a : α) (m : ) (n : ) :
        Commute (m * a) (n * a)
        @[deprecated Commute.intCast_mul_right]
        theorem Commute.cast_int_mul_right {α : Type u_3} [Ring α] {a : α} {b : α} (h : Commute a b) (m : ) :
        Commute a (m * b)

        Alias of Commute.intCast_mul_right.

        @[deprecated Commute.intCast_mul_left]
        theorem Commute.cast_int_mul_left {α : Type u_3} [Ring α] {a : α} {b : α} (h : Commute a b) (m : ) :
        Commute (m * a) b

        Alias of Commute.intCast_mul_left.

        @[deprecated Commute.intCast_mul_intCast_mul]
        theorem Commute.cast_int_mul_cast_int_mul {α : Type u_3} [Ring α] {a : α} {b : α} (h : Commute a b) (m : ) (n : ) :
        Commute (m * a) (n * b)

        Alias of Commute.intCast_mul_intCast_mul.

        @[deprecated Commute.self_intCast_mul]
        theorem Commute.self_cast_int_mul {α : Type u_3} [Ring α] (a : α) (n : ) :
        Commute a (n * a)

        Alias of Commute.self_intCast_mul.

        @[deprecated Commute.intCast_mul_self]
        theorem Commute.cast_int_mul_self {α : Type u_3} [Ring α] (a : α) (n : ) :
        Commute (n * a) a

        Alias of Commute.intCast_mul_self.

        @[deprecated Commute.self_intCast_mul_intCast_mul]
        theorem Commute.self_cast_int_mul_cast_int_mul {α : Type u_3} [Ring α] (a : α) (m : ) (n : ) :
        Commute (m * a) (n * a)

        Alias of Commute.self_intCast_mul_intCast_mul.

        theorem AddMonoidHom.ext_int_iff {A : Type u_5} [AddMonoid A] {f : →+ A} {g : →+ A} :
        f = g f 1 = g 1
        theorem AddMonoidHom.ext_int {A : Type u_5} [AddMonoid A] {f : →+ A} {g : →+ A} (h1 : f 1 = g 1) :
        f = g

        Two additive monoid homomorphisms f, g from to an additive monoid are equal if f 1 = g 1.

        theorem AddMonoidHom.eq_intCastAddHom {A : Type u_5} [AddGroupWithOne A] (f : →+ A) (h1 : f 1 = 1) :
        @[deprecated AddMonoidHom.eq_intCastAddHom]
        theorem AddMonoidHom.eq_int_castAddHom {A : Type u_5} [AddGroupWithOne A] (f : →+ A) (h1 : f 1 = 1) :

        Alias of AddMonoidHom.eq_intCastAddHom.

        theorem eq_intCast' {F : Type u_1} {α : Type u_3} [AddGroupWithOne α] [FunLike F α] [AddMonoidHomClass F α] (f : F) (h₁ : f 1 = 1) (n : ) :
        f n = n
        @[simp]
        theorem zsmul_one {α : Type u_3} [AddGroupWithOne α] (n : ) :
        n 1 = n
        theorem MonoidHom.ext_mint_iff {M : Type u_5} [Monoid M] {f : Multiplicative →* M} {g : Multiplicative →* M} :
        f = g f (Multiplicative.ofAdd 1) = g (Multiplicative.ofAdd 1)
        theorem MonoidHom.ext_mint {M : Type u_5} [Monoid M] {f : Multiplicative →* M} {g : Multiplicative →* M} (h1 : f (Multiplicative.ofAdd 1) = g (Multiplicative.ofAdd 1)) :
        f = g
        theorem MonoidHom.ext_int_iff {M : Type u_5} [Monoid M] {f : →* M} {g : →* M} :
        f = g f (-1) = g (-1) f.comp Int.ofNatHom = g.comp Int.ofNatHom
        theorem MonoidHom.ext_int {M : Type u_5} [Monoid M] {f : →* M} {g : →* M} (h_neg_one : f (-1) = g (-1)) (h_nat : f.comp Int.ofNatHom = g.comp Int.ofNatHom) :
        f = g

        If two MonoidHoms agree on -1 and the naturals then they are equal.

        theorem MonoidWithZeroHom.ext_int_iff {M : Type u_5} [MonoidWithZero M] {f : →*₀ M} {g : →*₀ M} :
        f = g f (-1) = g (-1) f.comp Int.ofNatHom.toMonoidWithZeroHom = g.comp Int.ofNatHom.toMonoidWithZeroHom
        theorem MonoidWithZeroHom.ext_int {M : Type u_5} [MonoidWithZero M] {f : →*₀ M} {g : →*₀ M} (h_neg_one : f (-1) = g (-1)) (h_nat : f.comp Int.ofNatHom.toMonoidWithZeroHom = g.comp Int.ofNatHom.toMonoidWithZeroHom) :
        f = g

        If two MonoidWithZeroHoms agree on -1 and the naturals then they are equal.

        theorem ext_int' {F : Type u_1} {α : Type u_3} [MonoidWithZero α] [FunLike F α] [MonoidWithZeroHomClass F α] {f : F} {g : F} (h_neg_one : f (-1) = g (-1)) (h_pos : ∀ (n : ), 0 < nf n = g n) :
        f = g

        If two MonoidWithZeroHoms agree on -1 and the positive naturals then they are equal.

        def zmultiplesHom (β : Type u_4) [AddGroup β] :
        β ( →+ β)

        Additive homomorphisms from are defined by the image of 1.

        Equations
        • zmultiplesHom β = { toFun := fun (x : β) => { toFun := fun (n : ) => n x, map_zero' := , map_add' := }, invFun := fun (f : →+ β) => f 1, left_inv := , right_inv := }
        Instances For
          def zpowersHom (α : Type u_3) [Group α] :

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

          Equations
          Instances For
            @[simp]
            theorem zmultiplesHom_apply (β : Type u_4) [AddGroup β] (x : β) (n : ) :
            ((zmultiplesHom β) x) n = n x
            @[simp]
            theorem zmultiplesHom_symm_apply (β : Type u_4) [AddGroup β] (f : →+ β) :
            (zmultiplesHom β).symm f = f 1
            @[simp]
            theorem zpowersHom_apply (α : Type u_3) [Group α] (x : α) (n : Multiplicative ) :
            ((zpowersHom α) x) n = x ^ Multiplicative.toAdd n
            @[simp]
            theorem zpowersHom_symm_apply (α : Type u_3) [Group α] (f : Multiplicative →* α) :
            (zpowersHom α).symm f = f (Multiplicative.ofAdd 1)
            theorem MonoidHom.apply_mint (α : Type u_3) [Group α] (f : Multiplicative →* α) (n : Multiplicative ) :
            f n = f (Multiplicative.ofAdd 1) ^ Multiplicative.toAdd n
            theorem AddMonoidHom.apply_int (β : Type u_4) [AddGroup β] (f : →+ β) (n : ) :
            f n = n f 1
            def zmultiplesAddHom (β : Type u_4) [AddCommGroup β] :
            β ≃+ ( →+ β)

            If α is commutative, zmultiplesHom is an additive equivalence.

            Equations
            Instances For
              def zpowersMulHom (α : Type u_3) [CommGroup α] :

              If α is commutative, zpowersHom is a multiplicative equivalence.

              Equations
              Instances For
                @[simp]
                theorem zpowersMulHom_apply {α : Type u_3} [CommGroup α] (x : α) (n : Multiplicative ) :
                ((zpowersMulHom α) x) n = x ^ Multiplicative.toAdd n
                @[simp]
                theorem zpowersMulHom_symm_apply {α : Type u_3} [CommGroup α] (f : Multiplicative →* α) :
                (zpowersMulHom α).symm f = f (Multiplicative.ofAdd 1)
                @[simp]
                theorem zmultiplesAddHom_apply (β : Type u_4) [AddCommGroup β] (x : β) (n : ) :
                ((zmultiplesAddHom β) x) n = n x
                @[simp]
                theorem zmultiplesAddHom_symm_apply (β : Type u_4) [AddCommGroup β] (f : →+ β) :
                (zmultiplesAddHom β).symm f = f 1
                @[simp]
                theorem eq_intCast {F : Type u_1} {α : Type u_3} [NonAssocRing α] [FunLike F α] [RingHomClass F α] (f : F) (n : ) :
                f n = n
                @[simp]
                theorem map_intCast {F : Type u_1} {α : Type u_3} {β : Type u_4} [NonAssocRing α] [NonAssocRing β] [FunLike F α β] [RingHomClass F α β] (f : F) (n : ) :
                f n = n
                theorem RingHom.eq_intCast' {α : Type u_3} [NonAssocRing α] (f : →+* α) :
                theorem RingHom.ext_int {R : Type u_5} [NonAssocSemiring R] (f : →+* R) (g : →+* R) :
                f = g
                instance Pi.instIntCast {ι : Type u_2} {π : ιType u_5} [(i : ι) → IntCast (π i)] :
                IntCast ((i : ι) → π i)
                Equations
                • Pi.instIntCast = { intCast := fun (n : ) (x : ι) => n }
                theorem Pi.intCast_apply {ι : Type u_2} {π : ιType u_5} [(i : ι) → IntCast (π i)] (n : ) (i : ι) :
                n i = n
                @[simp]
                theorem Pi.intCast_def {ι : Type u_2} {π : ιType u_5} [(i : ι) → IntCast (π i)] (n : ) :
                n = fun (x : ι) => n
                @[deprecated Pi.intCast_apply]
                theorem Pi.int_apply {ι : Type u_2} {π : ιType u_5} [(i : ι) → IntCast (π i)] (n : ) (i : ι) :
                n i = n

                Alias of Pi.intCast_apply.

                @[deprecated Pi.intCast_def]
                theorem Pi.coe_int {ι : Type u_2} {π : ιType u_5} [(i : ι) → IntCast (π i)] (n : ) :
                n = fun (x : ι) => n

                Alias of Pi.intCast_def.

                theorem Sum.elim_intCast_intCast {α : Type u_5} {β : Type u_6} {γ : Type u_7} [IntCast γ] (n : ) :
                Sum.elim n n = n