Documentation

Mathlib.Algebra.Order.Group.Unbundled.Int

Facts about as an (unbundled) ordered group #

See note [foundational algebra order theory].

Recursors #

theorem Int.natCast_strictMono :
StrictMono fun (x : ) => x
@[deprecated Int.natCast_strictMono]
theorem Int.coe_nat_strictMono :
StrictMono fun (x : ) => x

Alias of Int.natCast_strictMono.

Miscellaneous lemmas #

theorem Int.abs_eq_natAbs (a : ) :
|a| = a.natAbs
@[simp]
theorem Int.natCast_natAbs (n : ) :
n.natAbs = |n|
theorem Int.natAbs_abs (a : ) :
|a|.natAbs = a.natAbs
theorem Int.sign_mul_abs (a : ) :
a.sign * |a| = a
theorem Int.natAbs_le_self_sq (a : ) :
a.natAbs a ^ 2
theorem Int.natAbs_le_self_pow_two (a : ) :
a.natAbs a ^ 2

Alias of Int.natAbs_le_self_sq.

theorem Int.le_self_sq (b : ) :
b b ^ 2
theorem Int.le_self_pow_two (b : ) :
b b ^ 2

Alias of Int.le_self_sq.

theorem Int.abs_natCast (n : ) :
|n| = n
theorem Int.natAbs_sub_pos_iff {i : } {j : } :
0 < (i - j).natAbs i j
theorem Int.natAbs_sub_ne_zero_iff {i : } {j : } :
(i - j).natAbs 0 i j
@[simp]
theorem Int.abs_lt_one_iff {a : } :
|a| < 1 a = 0
theorem Int.abs_le_one_iff {a : } :
|a| 1 a = 0 a = 1 a = -1
theorem Int.one_le_abs {z : } (h₀ : z 0) :
1 |z|

/ #

theorem Int.ediv_eq_zero_of_lt_abs {a : } {b : } (H1 : 0 a) (H2 : a < |b|) :
a / b = 0

mod #

@[simp]
theorem Int.emod_abs (a : ) (b : ) :
a % |b| = a % b
theorem Int.emod_lt (a : ) {b : } (H : b 0) :
a % b < |b|

properties of / and % #

theorem Int.abs_ediv_le_abs (a : ) (b : ) :
|a / b| |a|
theorem Int.abs_sign_of_nonzero {z : } (hz : z 0) :
|z.sign| = 1
theorem Int.sign_eq_ediv_abs (a : ) :
a.sign = a / |a|
@[simp]
theorem abs_zsmul_eq_zero {G : Type u_1} [AddGroup G] (a : G) (n : ) :
|n| a = 0 n a = 0
@[simp]
theorem zpow_abs_eq_one {G : Type u_1} [Group G] (a : G) (n : ) :
a ^ |n| = 1 a ^ n = 1