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
theorem Int.coe_nat_pos {n : } :
0 < n 0 < n
theorem Int.toNat_lt' {a : } {b : } (hb : b 0) :
Int.toNat a < b a < b
theorem Int.natMod_lt {a : } {b : } (hb : b 0) :
Int.natMod a b < b
@[simp]
theorem Int.cast_mul {α : Type u_1} [inst : NonAssocRing α] (m : ) (n : ) :
↑(m * n) = m * n
@[simp]
theorem Int.cast_ite {α : Type u_1} [inst : AddGroupWithOne α] (P : Prop) [inst : Decidable P] (m : ) (n : ) :
↑(if P then m else n) = if P then m else n
def Int.castAddHom (α : Type u_1) [inst : AddGroupWithOne α] :

coe : ℤ → α→ α as an AddMonoidHom.

Equations
  • Int.castAddHom α = { toZeroHom := { toFun := Int.cast, map_zero' := (_ : 0 = 0) }, map_add' := (_ : ∀ (m n : ), ↑(m + n) = m + n) }
@[simp]
theorem Int.coe_castAddHom {α : Type u_1} [inst : AddGroupWithOne α] :
↑(Int.castAddHom α) = fun x => x
def Int.castRingHom (α : Type u_1) [inst : NonAssocRing α] :

coe : ℤ → α→ α as a RingHom.

Equations
  • One or more equations did not get rendered due to their size.
@[simp]
theorem Int.coe_castRingHom {α : Type u_1} [inst : NonAssocRing α] :
↑(Int.castRingHom α) = fun x => x
theorem Int.cast_commute {α : Type u_1} [inst : NonAssocRing α] (m : ) (x : α) :
Commute (m) x
theorem Int.cast_comm {α : Type u_1} [inst : NonAssocRing α] (m : ) (x : α) :
m * x = x * m
theorem Int.commute_cast {α : Type u_1} [inst : NonAssocRing α] (x : α) (m : ) :
Commute x m
theorem Int.cast_mono {α : Type u_1} [inst : OrderedRing α] :
Monotone fun x => x
@[simp]
theorem Int.cast_nonneg {α : Type u_1} [inst : OrderedRing α] [inst : Nontrivial α] {n : } :
0 n 0 n
@[simp]
theorem Int.cast_le {α : Type u_1} [inst : OrderedRing α] [inst : Nontrivial α] {m : } {n : } :
m n m n
theorem Int.cast_strictMono {α : Type u_1} [inst : OrderedRing α] [inst : Nontrivial α] :
StrictMono fun x => x
@[simp]
theorem Int.cast_lt {α : Type u_1} [inst : OrderedRing α] [inst : Nontrivial α] {m : } {n : } :
m < n m < n
@[simp]
theorem Int.cast_nonpos {α : Type u_1} [inst : OrderedRing α] [inst : Nontrivial α] {n : } :
n 0 n 0
@[simp]
theorem Int.cast_pos {α : Type u_1} [inst : OrderedRing α] [inst : Nontrivial α] {n : } :
0 < n 0 < n
@[simp]
theorem Int.cast_lt_zero {α : Type u_1} [inst : OrderedRing α] [inst : Nontrivial α] {n : } :
n < 0 n < 0
@[simp]
theorem Int.cast_min {α : Type u_1} [inst : LinearOrderedRing α] {a : } {b : } :
↑(min a b) = min a b
@[simp]
theorem Int.cast_max {α : Type u_1} [inst : LinearOrderedRing α] {a : } {b : } :
↑(max a b) = max a b
@[simp]
theorem Int.cast_abs {α : Type u_1} [inst : LinearOrderedRing α] {a : } :
↑(abs a) = abs a
theorem Int.cast_one_le_of_pos {α : Type u_1} [inst : LinearOrderedRing α] {a : } (h : 0 < a) :
1 a
theorem Int.cast_le_neg_one_of_neg {α : Type u_1} [inst : LinearOrderedRing α] {a : } (h : a < 0) :
a -1
theorem Int.cast_le_neg_one_or_one_le_cast_of_ne_zero (α : Type u_1) [inst : LinearOrderedRing α] {n : } (hn : n 0) :
n -1 1 n
theorem Int.nneg_mul_add_sq_of_abs_le_one {α : Type u_1} [inst : LinearOrderedRing α] (n : ) {x : α} (hx : abs x 1) :
0 n * x + n * n
theorem Int.cast_natAbs {α : Type u_1} [inst : LinearOrderedRing α] (n : ) :
↑(Int.natAbs n) = ↑(abs n)
theorem Int.coe_int_dvd {α : Type u_1} [inst : CommRing α] (m : ) (n : ) (h : m n) :
m n
theorem AddMonoidHom.ext_int {A : Type u_1} [inst : 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_int_castAddHom {A : Type u_1} [inst : AddGroupWithOne A] (f : →+ A) (h1 : f 1 = 1) :
theorem eq_intCast' {F : Type u_2} {α : Type u_1} [inst : AddGroupWithOne α] [inst : AddMonoidHomClass F α] (f : F) (h₁ : f 1 = 1) (n : ) :
f n = n
theorem MonoidHom.ext_mint {M : Type u_1} [inst : Monoid M] {f : Multiplicative →* M} {g : Multiplicative →* M} (h1 : f (Multiplicative.ofAdd 1) = g (Multiplicative.ofAdd 1)) :
f = g
theorem MonoidHom.ext_int {M : Type u_1} [inst : Monoid M] {f : →* M} {g : →* M} (h_neg_one : f (-1) = g (-1)) (h_nat : MonoidHom.comp f Int.ofNatHom = MonoidHom.comp g Int.ofNatHom) :
f = g

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

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

theorem ext_int' {F : Type u_2} {α : Type u_1} [inst : MonoidWithZero α] [inst : 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.

@[simp]
theorem eq_intCast {F : Type u_1} {α : Type u_2} [inst : NonAssocRing α] [inst : RingHomClass F α] (f : F) (n : ) :
f n = n
@[simp]
theorem map_intCast {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : NonAssocRing α] [inst : NonAssocRing β] [inst : RingHomClass F α β] (f : F) (n : ) :
f n = n
theorem RingHom.eq_intCast' {α : Type u_1} [inst : NonAssocRing α] (f : →+* α) :
theorem RingHom.ext_int {R : Type u_1} [inst : NonAssocSemiring R] (f : →+* R) (g : →+* R) :
f = g
instance Pi.intCast {ι : Type u_1} {π : ιType u_2} [inst : (i : ι) → IntCast (π i)] :
IntCast ((i : ι) → π i)
Equations
  • Pi.intCast = { intCast := fun n x => n }
theorem Pi.int_apply {ι : Type u_2} {π : ιType u_1} [inst : (i : ι) → IntCast (π i)] (n : ) (i : ι) :
n i = n
@[simp]
theorem Pi.coe_int {ι : Type u_1} {π : ιType u_2} [inst : (i : ι) → IntCast (π i)] (n : ) :
n = fun x => n
theorem Sum.elim_intCast_intCast {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : IntCast γ] (n : ) :
Sum.elim n n = n

Order dual #

instance instIntCastOrderDual {α : Type u_1} [h : IntCast α] :
Equations
  • instIntCastOrderDual = h
Equations
  • instAddGroupWithOneOrderDual = h
Equations
  • instAddCommGroupWithOneOrderDual = h
@[simp]
theorem toDual_intCast {α : Type u_1} [inst : IntCast α] (n : ) :
OrderDual.toDual n = n
@[simp]
theorem ofDual_intCast {α : Type u_1} [inst : IntCast α] (n : ) :
↑(OrderDual.ofDual n) = n

Lexicographic order #

instance instIntCastLex {α : Type u_1} [h : IntCast α] :
Equations
  • instIntCastLex = h
Equations
  • instAddGroupWithOneLex = h
Equations
  • instAddCommGroupWithOneLex = h
@[simp]
theorem toLex_intCast {α : Type u_1} [inst : IntCast α] (n : ) :
toLex n = n
@[simp]
theorem ofLex_intCast {α : Type u_1} [inst : IntCast α] (n : ) :
↑(ofLex n) = n