mathlib documentation

data.pnat.basic

source
def pnat  :
Type

ℕ+ is the type of positive natural numbers. It is defined as a subtype, and the VM representation of ℕ+ is the same as ℕ because the proof is not stored.

Equations
source
@[instance]
def coe_pnat_nat  :
has_coe ℕ+ ℕ

Equations
source
@[instance]
def pnat.has_repr  :
has_repr ℕ+

Equations
source
def pnat.nat_pred (i : ℕ+) :
ℕ

Predecessor of a ℕ+, as a ℕ.

Equations
source
def nat.to_pnat (n : ℕ) (h : 0 < n . "exact_dec_trivial") :
ℕ+

Convert a natural number to a positive natural number. The positivity assumption is inferred by dec_trivial.

Equations
source
def nat.succ_pnat (n : ℕ) :
ℕ+

Write a successor as an element of ℕ+.

Equations
source
@[simp]
theorem nat.succ_pnat_coe (n : ℕ) :
↑(n.succ_pnat) = n.succ

source
theorem nat.succ_pnat_inj {n m : ℕ} (a : n.succ_pnat = m.succ_pnat) :
n = m

source
def nat.to_pnat' (n : ℕ) :
ℕ+

Convert a natural number to a pnat. n+1 is mapped to itself, and 0 becomes 1.

Equations
source
@[simp]
theorem nat.to_pnat'_coe (n : ℕ) :
↑(n.to_pnat') = ite (0 < n) n 1

source
@[instance]
def nat.primes.coe_pnat  :
has_coe nat.primes ℕ+

Equations
source
theorem nat.primes.coe_pnat_nat (p : nat.primes) :
↑↑p = ↑p

source
theorem nat.primes.coe_pnat_inj (p q : nat.primes) (a : ↑p = ↑q) :
p = q

source
@[instance]
def pnat.decidable_eq  :
decidable_eq ℕ+

We now define a long list of structures on ℕ+ induced by similar structures on ℕ. Most of these behave in a completely obvious way, but there are a few things to be said about subtraction, division and powers.

Equations
source
@[instance]
def pnat.decidable_linear_order  :
decidable_linear_order ℕ+

Equations
source
@[simp]
theorem pnat.mk_le_mk (n k : ℕ) (hn : 0 < n) (hk : 0 < k) :
⟨n, hn⟩ ≤ ⟨k, hk⟩ ↔ n ≤ k

source
@[simp]
theorem pnat.mk_lt_mk (n k : ℕ) (hn : 0 < n) (hk : 0 < k) :
⟨n, hn⟩ < ⟨k, hk⟩ ↔ n < k

source
@[simp]
theorem pnat.coe_le_coe (n k : ℕ+) :
↑n ≤ ↑k ↔ n ≤ k

source
@[simp]
theorem pnat.coe_lt_coe (n k : ℕ+) :
↑n < ↑k ↔ n < k

source
@[simp]
theorem pnat.pos (n : ℕ+) :
0 < ↑n

source
theorem pnat.eq {m n : ℕ+} (a : ↑m = ↑n) :
m = n

source
@[simp]
theorem pnat.coe_inj {m n : ℕ+} :
↑m = ↑n ↔ m = n

source
@[simp]
theorem pnat.mk_coe (n : ℕ) (h : 0 < n) :
↑⟨n, h⟩ = n

source
@[instance]
def pnat.add_comm_semigroup  :
add_comm_semigroup ℕ+

Equations
source
@[simp]
theorem pnat.add_coe (m n : ℕ+) :
↑(m + n) = ↑m + ↑n

source
@[instance]
def pnat.coe_add_hom  :
is_add_hom coe

source
@[instance]
def pnat.add_left_cancel_semigroup  :
add_left_cancel_semigroup ℕ+

Equations
source
@[instance]
def pnat.add_right_cancel_semigroup  :
add_right_cancel_semigroup ℕ+

Equations
source
@[simp]
theorem pnat.ne_zero (n : ℕ+) :
↑n ≠ 0

source
theorem pnat.to_pnat'_coe {n : ℕ} (a : 0 < n) :
↑(n.to_pnat') = n

source
@[simp]
theorem pnat.coe_to_pnat' (n : ℕ+) :
↑n.to_pnat' = n

source
@[instance]
def pnat.comm_monoid  :
comm_monoid ℕ+

Equations
source
theorem pnat.lt_add_one_iff {a b : ℕ+} :
a < b + 1 ↔ a ≤ b

source
theorem pnat.add_one_le_iff {a b : ℕ+} :
a + 1 ≤ b ↔ a < b

source
@[simp]
theorem pnat.one_le (n : ℕ+) :
1 ≤ n

source
@[instance]
def pnat.order_bot  :
order_bot ℕ+

Equations
source
@[simp]
theorem pnat.bot_eq_zero  :
⊥ = 1

source
@[instance]
def pnat.inhabited  :
inhabited ℕ+

Equations
source
@[simp]
theorem pnat.mk_one {h : 0 < 1} :
⟨1, h⟩ = 1

source
@[simp]
theorem pnat.mk_bit0 (n : ℕ) {h : 0 < bit0 n} :
⟨bit0 n, h⟩ = bit0 ⟨n, _⟩

source
@[simp]
theorem pnat.mk_bit1 (n : ℕ) {h : 0 < bit1 n} {k : 0 < n} :
⟨bit1 n, h⟩ = bit1 ⟨n, k⟩

source
@[simp]
theorem pnat.bit0_le_bit0 (n m : ℕ+) :
bit0 n ≤ bit0 m ↔ bit0 ↑n ≤ bit0 ↑m

source
@[simp]
theorem pnat.bit0_le_bit1 (n m : ℕ+) :
bit0 n ≤ bit1 m ↔ bit0 ↑n ≤ bit1 ↑m

source
@[simp]
theorem pnat.bit1_le_bit0 (n m : ℕ+) :
bit1 n ≤ bit0 m ↔ bit1 ↑n ≤ bit0 ↑m

source
@[simp]
theorem pnat.bit1_le_bit1 (n m : ℕ+) :
bit1 n ≤ bit1 m ↔ bit1 ↑n ≤ bit1 ↑m

source
@[simp]
theorem pnat.one_coe  :
↑1 = 1

source
@[simp]
theorem pnat.mul_coe (m n : ℕ+) :
↑m * n = (↑m) * ↑n

source
@[instance]
def pnat.coe_mul_hom  :
is_monoid_hom coe

source
@[simp]
theorem pnat.coe_eq_one_iff {m : ℕ+} :
↑m = 1 ↔ m = 1

source
@[simp]
theorem pnat.coe_bit0 (a : ℕ+) :
↑(bit0 a) = bit0 ↑a

source
@[simp]
theorem pnat.coe_bit1 (a : ℕ+) :
↑(bit1 a) = bit1 ↑a

source
@[simp]
theorem pnat.pow_coe (m : ℕ+) (n : ℕ) :
↑(m ^ n) = ↑m ^ n

source
@[instance]
def pnat.left_cancel_semigroup  :
left_cancel_semigroup ℕ+

Equations
source
@[instance]
def pnat.right_cancel_semigroup  :
right_cancel_semigroup ℕ+

Equations
source
@[instance]
def pnat.ordered_cancel_comm_monoid  :
ordered_cancel_comm_monoid ℕ+

Equations
source
@[instance]
def pnat.distrib  :
distrib ℕ+

Equations
source
@[instance]
def pnat.has_sub  :
has_sub ℕ+

Subtraction a - b is defined in the obvious way when a > b, and by a - b = 1 if a ≤ b.

Equations
source
theorem pnat.sub_coe (a b : ℕ+) :
↑(a - b) = ite (b < a) (↑a - ↑b) 1

source
theorem pnat.add_sub_of_lt {a b : ℕ+} (a_1 : a < b) :
a + (b - a) = b

source
def pnat.mod_div_aux (a : ℕ+) (a_1 a_2 : ℕ) :
ℕ+ × ℕ

We define m % k and m / k in the same way as for nat except that when m = n * k we take m % k = k and m / k = n - 1. This ensures that m % k is always positive and m = (m % k) + k * (m / k) in all cases. Later we define a function div_exact which gives the usual m / k in the case where k divides m.

Equations
source
theorem pnat.mod_div_aux_spec (k : ℕ+) (r q : ℕ) (h : ¬(r = 0 ∧ q = 0)) :
↑((k.mod_div_aux r q).fst) + (↑k) * (k.mod_div_aux r q).snd = r + (↑k) * q

source
def pnat.mod_div (m k : ℕ+) :
ℕ+ × ℕ

Equations
source
def pnat.mod (m k : ℕ+) :
ℕ+

Equations
source
def pnat.div (m k : ℕ+) :
ℕ

Equations
source
theorem pnat.mod_add_div (m k : ℕ+) :
↑m = ↑(m.mod k) + (↑k) * m.div k

source
theorem pnat.mod_coe (m k : ℕ+) :
↑(m.mod k) = ite (↑m % ↑k = 0) ↑k (↑m % ↑k)

source
theorem pnat.div_coe (m k : ℕ+) :
m.div k = ite (↑m % ↑k = 0) (↑m / ↑k).pred (↑m / ↑k)

source
theorem pnat.mod_le (m k : ℕ+) :
m.mod k ≤ m ∧ m.mod k ≤ k

source
theorem pnat.dvd_iff {k m : ℕ+} :
k ∣ m ↔ ↑k ∣ ↑m

source
theorem pnat.dvd_iff' {k m : ℕ+} :
k ∣ m ↔ m.mod k = k

source
theorem pnat.le_of_dvd {m n : ℕ+} (a : m ∣ n) :
m ≤ n

source
def pnat.div_exact {m k : ℕ+} (h : k ∣ m) :
ℕ+

Equations
source
theorem pnat.mul_div_exact {m k : ℕ+} (h : k ∣ m) :
k * pnat.div_exact h = m

source
theorem pnat.dvd_antisymm {m n : ℕ+} (a : m ∣ n) (a_1 : n ∣ m) :
m = n

source
theorem pnat.dvd_one_iff (n : ℕ+) :
n ∣ 1 ↔ n = 1

source
def pnat.gcd (n m : ℕ+) :
ℕ+

Equations
source
def pnat.lcm (n m : ℕ+) :
ℕ+

Equations
source
@[simp]
theorem pnat.gcd_coe (n m : ℕ+) :
↑(n.gcd m) = ↑n.gcd ↑m

source
@[simp]
theorem pnat.lcm_coe (n m : ℕ+) :
↑(n.lcm m) = ↑n.lcm ↑m

source
theorem pnat.gcd_dvd_left (n m : ℕ+) :
n.gcd m ∣ n

source
theorem pnat.gcd_dvd_right (n m : ℕ+) :
n.gcd m ∣ m

source
theorem pnat.dvd_gcd {m n k : ℕ+} (hm : k ∣ m) (hn : k ∣ n) :
k ∣ m.gcd n

source
theorem pnat.dvd_lcm_left (n m : ℕ+) :
n ∣ n.lcm m

source
theorem pnat.dvd_lcm_right (n m : ℕ+) :
m ∣ n.lcm m

source
theorem pnat.lcm_dvd {m n k : ℕ+} (hm : m ∣ k) (hn : n ∣ k) :
m.lcm n ∣ k

source
theorem pnat.gcd_mul_lcm (n m : ℕ+) :
(n.gcd m) * n.lcm m = n * m

source
theorem pnat.eq_one_of_lt_two {n : ℕ+} (a : n < 2) :
n = 1

Prime numbers

source
def pnat.prime (p : ℕ+) :
Prop

Equations
source
theorem pnat.prime.one_lt {p : ℕ+} (a : p.prime) :
1 < p

source
theorem pnat.prime_two  :
2.prime

source
theorem pnat.dvd_prime {p m : ℕ+} (pp : p.prime) :
m ∣ p ↔ m = 1 ∨ m = p

source
theorem pnat.prime.ne_one {p : ℕ+} (a : p.prime) :
p ≠ 1

source
@[simp]
theorem pnat.not_prime_one  :
¬1.prime

source
theorem pnat.prime.not_dvd_one {p : ℕ+} (a : p.prime) :
¬p ∣ 1

source
theorem pnat.exists_prime_and_dvd {n : ℕ+} (a : 2 ≤ n) :
∃ (p : ℕ+), p.prime ∧ p ∣ n

Coprime numbers and gcd

source
def pnat.coprime (m n : ℕ+) :
Prop

Two pnats are coprime if their gcd is 1.

Equations
source
@[simp]
theorem pnat.coprime_coe {m n : ℕ+} :
↑m.coprime ↑n ↔ m.coprime n

source
theorem pnat.coprime.mul {k m n : ℕ+} (a : m.coprime k) (a_1 : n.coprime k) :
(m * n).coprime k

source
theorem pnat.coprime.mul_right {k m n : ℕ+} (a : k.coprime m) (a_1 : k.coprime n) :
k.coprime (m * n)

source
theorem pnat.gcd_comm {m n : ℕ+} :
m.gcd n = n.gcd m

source
theorem pnat.gcd_eq_left_iff_dvd {m n : ℕ+} :
m ∣ n ↔ m.gcd n = m

source
theorem pnat.gcd_eq_right_iff_dvd {m n : ℕ+} :
m ∣ n ↔ n.gcd m = m

source
theorem pnat.coprime.gcd_mul_left_cancel (m : ℕ+) {n k : ℕ+} (a : k.coprime n) :
(k * m).gcd n = m.gcd n

source
theorem pnat.coprime.gcd_mul_right_cancel (m : ℕ+) {n k : ℕ+} (a : k.coprime n) :
(m * k).gcd n = m.gcd n

source
theorem pnat.coprime.gcd_mul_left_cancel_right (m : ℕ+) {n k : ℕ+} (a : k.coprime m) :
m.gcd (k * n) = m.gcd n

source
theorem pnat.coprime.gcd_mul_right_cancel_right (m : ℕ+) {n k : ℕ+} (a : k.coprime m) :
m.gcd (n * k) = m.gcd n

source
@[simp]
theorem pnat.one_gcd {n : ℕ+} :
1.gcd n = 1

source
@[simp]
theorem pnat.gcd_one {n : ℕ+} :
n.gcd 1 = 1

source
theorem pnat.coprime.symm {m n : ℕ+} (a : m.coprime n) :
n.coprime m

source
@[simp]
theorem pnat.one_coprime {n : ℕ+} :
1.coprime n

source
@[simp]
theorem pnat.coprime_one {n : ℕ+} :
n.coprime 1

source
theorem pnat.coprime.coprime_dvd_left {m k n : ℕ+} (a : m ∣ k) (a_1 : k.coprime n) :
m.coprime n

source
theorem pnat.coprime.factor_eq_gcd_left {a b m n : ℕ+} (cop : m.coprime n) (am : a ∣ m) (bn : b ∣ n) :
a = (a * b).gcd m

source
theorem pnat.coprime.factor_eq_gcd_right {a b m n : ℕ+} (cop : m.coprime n) (am : a ∣ m) (bn : b ∣ n) :
a = (b * a).gcd m

source
theorem pnat.coprime.factor_eq_gcd_left_right {a b m n : ℕ+} (cop : m.coprime n) (am : a ∣ m) (bn : b ∣ n) :
a = m.gcd (a * b)

source
theorem pnat.coprime.factor_eq_gcd_right_right {a b m n : ℕ+} (cop : m.coprime n) (am : a ∣ m) (bn : b ∣ n) :
a = m.gcd (b * a)

source
theorem pnat.coprime.gcd_mul (k : ℕ+) {m n : ℕ+} (h : m.coprime n) :
k.gcd (m * n) = (k.gcd m) * k.gcd n

source
theorem pnat.gcd_eq_left {m n : ℕ+} (a : m ∣ n) :
m.gcd n = m

source
theorem pnat.coprime.pow {m n : ℕ+} (k l : ℕ) (h : m.coprime n) :
(m ^ k).coprime (n ^ l)