Documentation

Mathlib.Algebra.Ring.Int

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.

@[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.

Equations
Equations
Equations

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
@[simp]
theorem Int.even_or_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)
Equations
theorem Int.even_add' {m : } {n : } :
Even (m + n) (Odd m Odd n)
@[simp, deprecated]
theorem Int.not_even_bit1 (n : ) :
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 nEven n.natAbs

Alias of the reverse direction of Int.natAbs_even.

theorem Odd.natAbs {n : } :
Odd nOdd 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 n2 * (n / 2) + 1 = n
theorem Int.ediv_two_mul_two_add_one_of_odd {n : } :
Odd nn / 2 * 2 + 1 = n
theorem Int.add_one_ediv_two_mul_two_of_odd {n : } :
Odd n1 + n / 2 * 2 = n
theorem Int.two_mul_ediv_two_of_odd {n : } (h : Odd n) :
2 * (n / 2) = n - 1