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].

Instances

instance Nat.instAddCancelCommMonoid : AddCancelCommMonoid ℕ

Equations

• Nat.instAddCancelCommMonoid = AddCancelCommMonoid.mk ⋯

instance Nat.instCommMonoid : CommMonoid ℕ

Equations

• Nat.instCommMonoid = CommMonoid.mk Nat.mul_comm

Extra instances to short-circuit type class resolution

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

instance Nat.instAddCommMonoid : AddCommMonoid ℕ

Equations

• Nat.instAddCommMonoid = inferInstance

instance Nat.instAddMonoid : AddMonoid ℕ

Equations

• Nat.instAddMonoid = inferInstance

instance Nat.instMonoid : Monoid ℕ

Equations

• Nat.instMonoid = inferInstance

instance Nat.instCommSemigroup : CommSemigroup ℕ

Equations

• Nat.instCommSemigroup = inferInstance

instance Nat.instSemigroup : Semigroup ℕ

Equations

• Nat.instSemigroup = inferInstance

instance Nat.instAddCommSemigroup : AddCommSemigroup ℕ

Equations

• Nat.instAddCommSemigroup = inferInstance

instance Nat.instAddSemigroup : AddSemigroup ℕ

Equations

• Nat.instAddSemigroup = inferInstance

Miscellaneous lemmas

@[simp]

theorem Nat.nsmul_eq_mul (m : ℕ) (n : ℕ) : m • n = m * n

theorem Nat.toAdd_pow (a : Multiplicative ℕ) (b : ℕ) : Multiplicative.toAdd (a ^ b) = Multiplicative.toAdd a * b

@[simp]

theorem Nat.ofAdd_mul (a : ℕ) (b : ℕ) : Multiplicative.ofAdd (a * b) = Multiplicative.ofAdd a ^ b

Parity

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

instance Nat.instDecidablePredEven : DecidablePred Even

Equations

• x.instDecidablePredEven = decidable_of_iff (x % 2 = 0) ⋯

instance Nat.instDecidablePredIsSquare : DecidablePred IsSquare

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

Equations

• m.instDecidablePredIsSquare = decidable_of_iff' (m.sqrt * m.sqrt = m) ⋯

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.not_even_one : ¬Even 1

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_add_one (n : ℕ) : ¬2 ∣ 2 * n + 1

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 n → 2 * (n / 2) = n

theorem Nat.div_two_mul_two_of_even {n : ℕ} : Even n → n / 2 * 2 = n

Units

theorem Nat.units_eq_one (u : ℕˣ) : u = 1

theorem Nat.addUnits_eq_zero (u : AddUnits ℕ) : u = 0

@[simp]

theorem Nat.isUnit_iff {n : ℕ} : IsUnit n ↔ n = 1

instance Nat.unique_units : Unique ℕˣ

Equations

• Nat.unique_units = { default := 1, uniq := Nat.units_eq_one }

instance Nat.unique_addUnits : Unique (AddUnits ℕ)

Equations

• Nat.unique_addUnits = { default := 0, uniq := Nat.addUnits_eq_zero }