Documentation

Mathlib.Algebra.Group.Int

The integers form a group #

This file contains the additive group and multiplicative monoid instances on the integers.

See note [foundational algebra order theory].

Instances #

Extra instances to short-circuit type class resolution #

These also prevent non-computable instances like Int.normedCommRing being used to construct these instances non-computably.

Equations
Equations
Equations
Equations

Miscellaneous lemmas #

theorem Int.toAdd_pow (a : Multiplicative ) (b : ) :
Multiplicative.toAdd (a ^ b) = Multiplicative.toAdd a * b
theorem Int.toAdd_zpow (a : Multiplicative ) (b : ) :
Multiplicative.toAdd (a ^ b) = Multiplicative.toAdd a * b
@[simp]
theorem Int.ofAdd_mul (a : ) (b : ) :
Multiplicative.ofAdd (a * b) = Multiplicative.ofAdd a ^ b

Units #

theorem Int.units_natAbs (u : ˣ) :
(↑u).natAbs = 1
@[simp]
theorem Int.natAbs_of_isUnit {u : } (hu : IsUnit u) :
u.natAbs = 1
theorem Int.isUnit_eq_one_or {u : } (hu : IsUnit u) :
u = 1 u = -1
theorem Int.isUnit_ne_iff_eq_neg {u : } {v : } (hu : IsUnit u) (hv : IsUnit v) :
u v u = -v
theorem Int.isUnit_eq_or_eq_neg {u : } {v : } (hu : IsUnit u) (hv : IsUnit v) :
u = v u = -v
theorem Int.isUnit_iff {u : } :
IsUnit u u = 1 u = -1
theorem Int.eq_one_or_neg_one_of_mul_eq_one {u : } {v : } (h : u * v = 1) :
u = 1 u = -1
theorem Int.eq_one_or_neg_one_of_mul_eq_one' {u : } {v : } (h : u * v = 1) :
u = 1 v = 1 u = -1 v = -1
theorem Int.eq_of_mul_eq_one {u : } {v : } (h : u * v = 1) :
u = v
theorem Int.mul_eq_one_iff_eq_one_or_neg_one {u : } {v : } :
u * v = 1 u = 1 v = 1 u = -1 v = -1
theorem Int.eq_one_or_neg_one_of_mul_eq_neg_one' {u : } {v : } (h : u * v = -1) :
u = 1 v = -1 u = -1 v = 1
theorem Int.mul_eq_neg_one_iff_eq_one_or_neg_one {u : } {v : } :
u * v = -1 u = 1 v = -1 u = -1 v = 1
theorem Int.isUnit_iff_natAbs_eq {u : } :
IsUnit u u.natAbs = 1
theorem Int.IsUnit.natAbs_eq {u : } :
IsUnit uu.natAbs = 1

Alias of the forward direction of Int.isUnit_iff_natAbs_eq.

theorem Int.isUnit_mul_self {u : } (hu : IsUnit u) :
u * u = 1
theorem Int.isUnit_add_isUnit_eq_isUnit_add_isUnit {a : } {b : } {c : } {d : } (ha : IsUnit a) (hb : IsUnit b) (hc : IsUnit c) (hd : IsUnit d) :
a + b = c + d a = c b = d a = d b = c
theorem Int.eq_one_or_neg_one_of_mul_eq_neg_one {u : } {v : } (h : u * v = -1) :
u = 1 u = -1

Parity #

@[simp]
theorem Int.emod_two_ne_one {n : } :
¬n % 2 = 1 n % 2 = 0
@[simp]
theorem Int.one_emod_two :
1 % 2 = 1
theorem Int.emod_two_ne_zero {n : } :
¬n % 2 = 0 n % 2 = 1
theorem Int.even_iff {n : } :
Even n n % 2 = 0
theorem Int.not_even_iff {n : } :
¬Even n n % 2 = 1
@[simp]
theorem Int.two_dvd_ne_zero {n : } :
¬2 n n % 2 = 1
Equations

IsSquare can be decided on by checking against the square root.

Equations
@[simp]
theorem Int.even_add {m : } {n : } :
Even (m + n) (Even m Even n)
theorem Int.even_sub {m : } {n : } :
Even (m - n) (Even m Even n)
theorem Int.even_add_one {n : } :
Even (n + 1) ¬Even n
theorem Int.even_sub_one {n : } :
Even (n - 1) ¬Even n
theorem Int.even_mul {m : } {n : } :
Even (m * n) Even m Even n
theorem Int.even_pow {m : } {n : } :
Even (m ^ n) Even m n 0
theorem Int.even_pow' {m : } {n : } (h : n 0) :
Even (m ^ n) Even m
@[simp]
theorem Int.even_coe_nat (n : ) :
Even n Even n
theorem Int.two_mul_ediv_two_of_even {n : } :
Even n2 * (n / 2) = n
theorem Int.ediv_two_mul_two_of_even {n : } :
Even nn / 2 * 2 = n
theorem zsmul_int_int (a : ) (b : ) :
a b = a * b
theorem zsmul_int_one (n : ) :
n 1 = n