The positive natural numbers #
This file contains the definitions, and basic results.
Most algebraic facts are deferred to Data.PNat.Basic
, as they need more imports.
ℕ+
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
- «termℕ+» = Lean.ParserDescr.node `termℕ+ 1024 (Lean.ParserDescr.symbol "ℕ+")
Instances For
Equations
- instReprPNat = { reprPrec := fun (n : ℕ+) (n' : ℕ) => reprPrec (↑n) n' }
Equations
- instOfNatPNatOfNeZeroNat n = { ofNat := ⟨n, ⋯⟩ }
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
- PNat.instWellFoundedRelation = measure fun (a : ℕ+) => ↑a
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
Instances For
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
.
Instances For
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
- m.div k = (m.modDiv k).2