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