Documentation

Mathlib.Algebra.Order.Ring.Int

The integers form a linear ordered ring #

This file contains:

Recursors #

Extra instances to short-circuit type class resolution #

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

Equations
Equations

Miscellaneous lemmas #

theorem Int.isCompl_even_odd :
IsCompl {n : | Even n} {n : | Odd n}
theorem Nat.cast_natAbs {α : Type u_1} [AddGroupWithOne α] (n : ) :
n.natAbs = |n|
theorem Int.cast_mul_eq_zsmul_cast {α : Type u_1} [AddCommGroupWithOne α] (m : ) (n : ) :
(m * n) = m n

Note this holds in marginally more generality than Int.cast_mul

theorem Int.two_le_iff_pos_of_even {m : } (even : Even m) :
2 m 0 < m
theorem Int.add_two_le_iff_lt_of_even_sub {m : } {n : } (even : Even (n - m)) :
m + 2 n m < n
theorem bit0_mul {R : Type u_1} [NonUnitalNonAssocRing R] (n : R) (r : R) :
bit0 n * r = 2 (n * r)
theorem mul_bit0 {R : Type u_1} [NonUnitalNonAssocRing R] (n : R) (r : R) :
r * bit0 n = 2 (r * n)
theorem bit1_mul {R : Type u_1} [NonAssocRing R] (n : R) (r : R) :
bit1 n * r = 2 (n * r) + r
theorem mul_bit1 {R : Type u_1} [NonAssocRing R] {n : R} {r : R} :
r * bit1 n = 2 (r * n) + r