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} [IntCast α] (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
        Instances For
          @[simp]
          theorem Int.coe_castAddHom {α : Type u_3} [AddGroupWithOne α] :
          (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
            Instances For
              @[simp]
              theorem Int.coe_castRingHom {α : Type u_3} [NonAssocRing α] :
              (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} [Ring α] (m n : ) (h : m n) :
              m n
              @[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
              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)
              @[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
              theorem Commute.intCast_mul_right {α : Type u_3} [Ring α] {a b : α} (h : Commute a b) (m : ) :
              Commute a (m * b)
              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)
              theorem AddMonoidHom.ext_int {A : Type u_5} [AddMonoid A] {f 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.ext_int_iff {A : Type u_5} [AddMonoid A] {f g : →+ A} :
              f = g f 1 = g 1
              theorem AddMonoidHom.eq_intCastAddHom {A : Type u_5} [AddGroupWithOne A] (f : →+ A) (h1 : f 1 = 1) :
              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
              theorem map_intCast' {F : Type u_1} {α : Type u_3} {β : Type u_4} [AddGroupWithOne α] [AddGroupWithOne β] [FunLike F α β] [AddMonoidHomClass F α β] (f : F) (h₁ : f 1 = 1) (n : ) :
              f n = n

              This version is primed so that the RingHomClass versions aren't.

              theorem MonoidHom.ext_mint {M : Type u_5} [Monoid M] {f g : Multiplicative →* M} (h1 : f (Multiplicative.ofAdd 1) = g (Multiplicative.ofAdd 1)) :
              f = g
              theorem MonoidHom.ext_int {M : Type u_5} [Monoid M] {f 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 MonoidHom.ext_int_iff {M : Type u_5} [Monoid M] {f g : →* M} :
              f = g f (-1) = g (-1) f.comp Int.ofNatHom = g.comp Int.ofNatHom
              theorem MonoidWithZeroHom.ext_int {M : Type u_5} [MonoidWithZero M] {f 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 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
                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 ) :
                      @[simp]
                      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 ) :
                              @[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 : →+ β) :
                              @[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 g : →+* R) :
                              f = g