The natural numbers form a monoid #

This file contains the additive and multiplicative monoid instances on the natural numbers.

See note [foundational algebra order theory].

Equations

Extra instances to short-circuit type class resolution #

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

Equations
Equations
instance Nat.instMonoid :
Equations
Equations
Equations
Equations
Equations

Miscellaneous lemmas #

@[simp]
theorem Nat.nsmul_eq_mul (m : ) (n : ) :
m n = m * n
theorem Nat.toAdd_pow (a : ) (b : ) :
@[simp]
theorem Nat.ofAdd_mul (a : ) (b : ) :

Parity #

theorem Nat.even_iff {n : } :
Even n n % 2 = 0
Equations

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

Equations
theorem Nat.not_even_iff {n : } :
¬Even n n % 2 = 1
@[simp]
theorem Nat.two_dvd_ne_zero {n : } :
¬2 n n % 2 = 1
@[simp]
theorem Nat.even_add {m : } {n : } :
Even (m + n) (Even m Even n)
theorem Nat.even_add_one {n : } :
Even (n + 1) ¬Even n
theorem Nat.succ_mod_two_eq_zero_iff {m : } :
(m + 1) % 2 = 0 m % 2 = 1
theorem Nat.succ_mod_two_eq_one_iff {m : } :
(m + 1) % 2 = 1 m % 2 = 0
theorem Nat.two_not_dvd_two_mul_sub_one {n : } :
0 < n¬2 2 * n - 1
theorem Nat.even_sub {m : } {n : } (h : n m) :
Even (m - n) (Even m Even n)
theorem Nat.even_mul {m : } {n : } :
Even (m * n) Even m Even n
theorem Nat.even_pow {m : } {n : } :
Even (m ^ n) Even m n 0

If m and n are natural numbers, then the natural number m^n is even if and only if m is even and n is positive.

theorem Nat.even_pow' {m : } {n : } (h : n 0) :
Even (m ^ n) Even m
theorem Nat.even_mul_succ_self (n : ) :
Even (n * (n + 1))
theorem Nat.even_mul_pred_self (n : ) :
Even (n * (n - 1))
@[deprecated Nat.even_mul_pred_self]
theorem Nat.even_mul_self_pred (n : ) :
Even (n * (n - 1))

Alias of Nat.even_mul_pred_self.

theorem Nat.two_mul_div_two_of_even {n : } :
Even n2 * (n / 2) = n
theorem Nat.div_two_mul_two_of_even {n : } :
Even nn / 2 * 2 = n

Units #

theorem Nat.units_eq_one (u : ) :
u = 1
theorem Nat.addUnits_eq_zero (u : ) :
u = 0
@[simp]
theorem Nat.isUnit_iff {n : } :
n = 1
instance Nat.unique_units :
Equations
Equations