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

instance Int.instCommMonoid : CommMonoid ℤ

Equations

• Int.instCommMonoid = CommMonoid.mk Int.mul_comm

instance Int.instAddCommGroup : AddCommGroup ℤ

Equations

• Int.instAddCommGroup = AddCommGroup.mk Int.add_comm

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.

instance Int.instAddCommMonoid : AddCommMonoid ℤ

Equations

• Int.instAddCommMonoid = inferInstance

instance Int.instAddMonoid : AddMonoid ℤ

Equations

• Int.instAddMonoid = inferInstance

instance Int.instMonoid : Monoid ℤ

Equations

• Int.instMonoid = inferInstance

instance Int.instCommSemigroup : CommSemigroup ℤ

Equations

• Int.instCommSemigroup = inferInstance

instance Int.instSemigroup : Semigroup ℤ

Equations

• Int.instSemigroup = inferInstance

instance Int.instAddGroup : AddGroup ℤ

Equations

• Int.instAddGroup = inferInstance

instance Int.instAddCommSemigroup : AddCommSemigroup ℤ

Equations

• Int.instAddCommSemigroup = inferInstance

instance Int.instAddSemigroup : AddSemigroup ℤ

Equations

• Int.instAddSemigroup = inferInstance

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 u → u.natAbs = 1

Alias of the forward direction of Int.isUnit_iff_natAbs_eq.

theorem Int.ofNat_isUnit {n : ℕ} : IsUnit ↑n ↔ IsUnit n

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

instance Int.instDecidablePredEven : DecidablePred Even

Equations

• x.instDecidablePredEven = decidable_of_iff (x % 2 = 0) ⋯

instance Int.instDecidablePredIsSquare : DecidablePred IsSquare

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

Equations

• m.instDecidablePredIsSquare = decidable_of_iff' (Int.sqrt m * Int.sqrt m = m) ⋯

@[simp]

theorem Int.not_even_one : ¬Even 1

theorem Int.even_add {m : ℤ} {n : ℤ} : Even (m + n) ↔ (Even m ↔ Even n)

theorem Int.two_not_dvd_two_mul_add_one (n : ℤ) : ¬2 ∣ 2 * n + 1

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 n → 2 * (n / 2) = n

theorem Int.ediv_two_mul_two_of_even {n : ℤ} : Even n → n / 2 * 2 = n

theorem zsmul_int_int (a : ℤ) (b : ℤ) : a • b = a * b

theorem zsmul_int_one (n : ℤ) : n • 1 = n