mathlib documentation

data.pnat.basic

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
@[instance]

Equations
@[instance]

Equations
def pnat.nat_pred  :
ℕ+

Predecessor of a ℕ+, as a .

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

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

Equations
def nat.succ_pnat  :
ℕ+

Write a successor as an element of ℕ+.

Equations
@[simp]
theorem nat.succ_pnat_coe (n : ) :

theorem nat.succ_pnat_inj {n m : } :
n.succ_pnat = m.succ_pnatn = m

def nat.to_pnat'  :
ℕ+

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

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

@[instance]

Equations
theorem nat.primes.coe_pnat_inj (p q : nat.primes) :
p = qp = q

@[instance]

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
@[simp]
theorem pnat.mk_le_mk (n k : ) (hn : 0 < n) (hk : 0 < k) :
n, hn⟩ k, hk⟩ n k

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

@[simp]
theorem pnat.coe_le_coe (n k : ℕ+) :
n k n k

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

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

theorem pnat.eq {m n : ℕ+} :
m = nm = n

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

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

@[instance]

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

@[instance]

@[simp]
theorem pnat.ne_zero (n : ℕ+) :
n 0

theorem pnat.to_pnat'_coe {n : } :
0 < n(n.to_pnat') = n

@[simp]
theorem pnat.coe_to_pnat' (n : ℕ+) :

@[instance]

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

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

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

@[instance]

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

@[instance]

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

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

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

@[simp]
theorem pnat.bit0_le_bit0 (n m : ℕ+) :

@[simp]
theorem pnat.bit0_le_bit1 (n m : ℕ+) :

@[simp]
theorem pnat.bit1_le_bit0 (n m : ℕ+) :

@[simp]
theorem pnat.bit1_le_bit1 (n m : ℕ+) :

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

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

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

@[simp]
theorem pnat.coe_bit0 (a : ℕ+) :

@[simp]
theorem pnat.coe_bit1 (a : ℕ+) :

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

@[instance]

Equations
@[instance]

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

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

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

@[instance]

Equations
theorem pnat.strong_induction_on {p : ℕ+ → Prop} (n : ℕ+) :
(∀ (k : ℕ+), (∀ (m : ℕ+), m < kp m)p k)p n

Strong induction on pnat.

theorem pnat.exists_eq_succ_of_ne_one {n : ℕ+} :
n 1(∃ (k : ℕ+), n = k + 1)

If (n : pnat) is different from 1, then it is the successor of some (k : pnat).

theorem pnat.case_strong_induction_on {p : ℕ+ → Prop} (a : ℕ+) :
p 1(∀ (n : ℕ+), (∀ (m : ℕ+), m np m)p (n + 1))p a

def pnat.mod_div_aux  :
ℕ+ℕ+ ×

We define m % k and m / k in the same way as for 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
theorem pnat.mod_div_aux_spec (k : ℕ+) (r q : ) :
¬(r = 0 q = 0)((k.mod_div_aux r q).fst) + (k) * (k.mod_div_aux r q).snd = r + (k) * q

def pnat.mod_div  :
ℕ+ℕ+ℕ+ ×

mod_div m k = (m % k, m / k). We define m % k and m / k in the same way as for 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
def pnat.mod  :
ℕ+ℕ+ℕ+

We define m % k in the same way as for except that when m = n * k we take m % k = k This ensures that m % k is always positive.

Equations
def pnat.div  :
ℕ+ℕ+

We define m / k in the same way as for except that when m = n * k we take m / k = n - 1. This ensures that 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
theorem pnat.mod_add_div (m k : ℕ+) :
m = (m.mod k) + (k) * m.div k

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

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

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

theorem pnat.dvd_iff {k m : ℕ+} :
k m k m

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

theorem pnat.le_of_dvd {m n : ℕ+} :
m nm n

def pnat.div_exact  :
ℕ+ℕ+ℕ+

If h : k | m, then k * (div_exact m k) = m. Note that this is not equal to m / k.

Equations
theorem pnat.mul_div_exact {m k : ℕ+} :
k mk * m.div_exact k = m

theorem pnat.dvd_antisymm {m n : ℕ+} :
m nn mm = n

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

theorem pnat.pos_of_div_pos {n : ℕ+} {a : } :
a n0 < a

def pnat.gcd  :
ℕ+ℕ+ℕ+

The greatest common divisor (gcd) of two positive natural numbers, viewed as positive natural number.

Equations
def pnat.lcm  :
ℕ+ℕ+ℕ+

The least common multiple (lcm) of two positive natural numbers, viewed as positive natural number.

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

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

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

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

theorem pnat.dvd_gcd {m n k : ℕ+} :
k mk nk m.gcd n

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

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

theorem pnat.lcm_dvd {m n k : ℕ+} :
m kn km.lcm n k

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

theorem pnat.eq_one_of_lt_two {n : ℕ+} :
n < 2n = 1

Prime numbers

def pnat.prime  :
ℕ+ → Prop

Primality predicate for ℕ+, defined in terms of nat.prime.

Equations
theorem pnat.prime.one_lt {p : ℕ+} :
p.prime1 < p

theorem pnat.prime_two  :

theorem pnat.dvd_prime {p m : ℕ+} :
p.prime(m p m = 1 m = p)

theorem pnat.prime.ne_one {p : ℕ+} :
p.primep 1

@[simp]
theorem pnat.not_prime_one  :

theorem pnat.prime.not_dvd_one {p : ℕ+} :
p.prime¬p 1

theorem pnat.exists_prime_and_dvd {n : ℕ+} :
2 n(∃ (p : ℕ+), p.prime p n)

Coprime numbers and gcd

def pnat.coprime  :
ℕ+ℕ+ → Prop

Two pnats are coprime if their gcd is 1.

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

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

theorem pnat.coprime.mul_right {k m n : ℕ+} :
k.coprime mk.coprime nk.coprime (m * n)

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

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

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

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

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

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

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

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

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

theorem pnat.coprime.symm {m n : ℕ+} :
m.coprime nn.coprime m

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

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

theorem pnat.coprime.coprime_dvd_left {m k n : ℕ+} :
m kk.coprime nm.coprime n

theorem pnat.coprime.factor_eq_gcd_left {a b m n : ℕ+} :
m.coprime na mb na = (a * b).gcd m

theorem pnat.coprime.factor_eq_gcd_right {a b m n : ℕ+} :
m.coprime na mb na = (b * a).gcd m

theorem pnat.coprime.factor_eq_gcd_left_right {a b m n : ℕ+} :
m.coprime na mb na = m.gcd (a * b)

theorem pnat.coprime.factor_eq_gcd_right_right {a b m n : ℕ+} :
m.coprime na mb na = m.gcd (b * a)

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

theorem pnat.gcd_eq_left {m n : ℕ+} :
m nm.gcd n = m

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