The integers are a ring

This file contains the commutative ring instance on ℤ.

See note [foundational algebra order theory].

Note

If this file needs to be split, please create an Algebra.Ring.Int folder and make the first file be Algebra.Ring.Int.Basic.

instance Int.instCommRing : CommRing ℤ

Equations

• Int.instCommRing = let __spread.0 := Int.instAddCommGroup; let __spread.1 := Int.instCommSemigroup; CommRing.mk ⋯

instance Int.instCancelCommMonoidWithZero : CancelCommMonoidWithZero ℤ

Equations

• Int.instCancelCommMonoidWithZero = CancelCommMonoidWithZero.mk

instance Int.instCharZero : CharZero ℤ

Equations

• Int.instCharZero = ⋯

instance Int.instMulDivCancelClass : MulDivCancelClass ℤ

Equations

• Int.instMulDivCancelClass = ⋯

@[simp]

theorem Int.cast_mul {α : Type u_1} [NonAssocRing α] (m : ℤ) (n : ℤ) : ↑(m * n) = ↑m * ↑n

@[simp]

theorem Int.cast_pow {R : Type u_1} [Ring R] (n : ℤ) (m : ℕ) : ↑(n ^ m) = ↑n ^ m

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.instCommSemiring : CommSemiring ℤ

Equations

• Int.instCommSemiring = inferInstance

instance Int.instSemiring : Semiring ℤ

Equations

• Int.instSemiring = inferInstance

instance Int.instRing : Ring ℤ

Equations

• Int.instRing = inferInstance

instance Int.instDistrib : Distrib ℤ

Equations

• Int.instDistrib = inferInstance

Miscellaneous lemmas

Units

theorem Int.units_eq_one_or (u : ℤˣ) : u = 1 ∨ u = -1

theorem Int.units_ne_iff_eq_neg {u : ℤˣ} {v : ℤˣ} : u ≠ v ↔ u = -v

Parity

theorem Int.odd_iff {n : ℤ} : Odd n ↔ n % 2 = 1

theorem Int.not_odd_iff {n : ℤ} : ¬Odd n ↔ n % 2 = 0

theorem Int.even_iff_not_odd {n : ℤ} : Even n ↔ ¬Odd n

@[simp]

theorem Int.odd_iff_not_even {n : ℤ} : Odd n ↔ ¬Even n

theorem Int.even_or_odd (n : ℤ) : Even n ∨ Odd n

theorem Int.even_or_odd' (n : ℤ) : ∃ (k : ℤ), n = 2 * k ∨ n = 2 * k + 1

theorem Int.even_xor'_odd (n : ℤ) : Xor' (Even n) (Odd n)

theorem Int.even_xor'_odd' (n : ℤ) : ∃ (k : ℤ), Xor' (n = 2 * k) (n = 2 * k + 1)

instance Int.instDecidablePredOdd : DecidablePred Odd

Equations

• x.instDecidablePredOdd = decidable_of_iff (¬Even x) ⋯

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

@[simp, deprecated]

theorem Int.not_even_bit1 (n : ℤ) : ¬Even (2 * n + 1)

theorem Int.not_even_two_mul_add_one (n : ℤ) : ¬Even (2 * n + 1)

theorem Int.even_sub' {m : ℤ} {n : ℤ} : Even (m - n) ↔ (Odd m ↔ Odd n)

theorem Int.odd_mul {m : ℤ} {n : ℤ} : Odd (m * n) ↔ Odd m ∧ Odd n

theorem Int.Odd.of_mul_left {m : ℤ} {n : ℤ} (h : Odd (m * n)) : Odd m

theorem Int.Odd.of_mul_right {m : ℤ} {n : ℤ} (h : Odd (m * n)) : Odd n

theorem Int.odd_pow {m : ℤ} {n : ℕ} : Odd (m ^ n) ↔ Odd m ∨ n = 0

theorem Int.odd_pow' {m : ℤ} {n : ℕ} (h : n ≠ 0) : Odd (m ^ n) ↔ Odd m

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

theorem Int.odd_add' {m : ℤ} {n : ℤ} : Odd (m + n) ↔ (Odd n ↔ Even m)

theorem Int.ne_of_odd_add {m : ℤ} {n : ℤ} (h : Odd (m + n)) : m ≠ n

theorem Int.odd_sub {m : ℤ} {n : ℤ} : Odd (m - n) ↔ (Odd m ↔ Even n)

theorem Int.odd_sub' {m : ℤ} {n : ℤ} : Odd (m - n) ↔ (Odd n ↔ Even m)

theorem Int.even_mul_succ_self (n : ℤ) : Even (n * (n + 1))

theorem Int.even_mul_pred_self (n : ℤ) : Even (n * (n - 1))

theorem Int.odd_coe_nat (n : ℕ) : Odd ↑n ↔ Odd n

@[simp]

theorem Int.natAbs_even {n : ℤ} : Even n.natAbs ↔ Even n

theorem Int.natAbs_odd {n : ℤ} : Odd n.natAbs ↔ Odd n

theorem Even.natAbs {n : ℤ} : Even n → Even n.natAbs

Alias of the reverse direction of Int.natAbs_even.

theorem Odd.natAbs {n : ℤ} : Odd n → Odd n.natAbs

Alias of the reverse direction of Int.natAbs_odd.

theorem Int.four_dvd_add_or_sub_of_odd {a : ℤ} {b : ℤ} (ha : Odd a) (hb : Odd b) : 4 ∣ a + b ∨ 4 ∣ a - b

theorem Int.two_mul_ediv_two_add_one_of_odd {n : ℤ} : Odd n → 2 * (n / 2) + 1 = n

theorem Int.ediv_two_mul_two_add_one_of_odd {n : ℤ} : Odd n → n / 2 * 2 + 1 = n

theorem Int.add_one_ediv_two_mul_two_of_odd {n : ℤ} : Odd n → 1 + n / 2 * 2 = n

theorem Int.two_mul_ediv_two_of_odd {n : ℤ} (h : Odd n) : 2 * (n / 2) = n - 1

@[simp]

theorem Int.isSquare_natCast_iff {n : ℕ} : IsSquare ↑n ↔ IsSquare n

@[simp]

theorem Int.isSquare_ofNat_iff {n : ℕ} : IsSquare (OfNat.ofNat n) ↔ IsSquare (OfNat.ofNat n)