Basic

📁 Source: Mathlib/Data/Num/Basic.lean

Statistics

Metric	Count
Definitions Num, add, bit, bit0, bit1, cmp, decidableLE, decidableLT, div, div2, gcd, gcdAux, instAdd, instDiv, instLE, instLT, instMod, instMul, instSub, mul, natSize, ofNat', ofZNum, ofZNum', ppred, pred, psub, size, sub, sub', succ, succ', toZNum, toZNumNeg, PosNum, add, bit, cmp, decidableLE, decidableLT, div', divMod, divModAux, instAdd, instLE, instLT, instMul, instOfNatHAddNatOfNat, instSub, isOne, mod', mul, natSize, ofNat, ofNatSucc, ofZNum, ofZNum', pred, pred', size, sub, sub', succ, abs, add, bit0, bit1, bitm1, cmp, decidableLE, decidableLT, div, gcd, instAdd, instDiv, instLE, instLT, instMod, instMul, instNeg, mul, ofInt', pred, succ, zNeg, castNum, castPosNum, castZNum, instDecidableEqNum, decEq, instDecidableEqPosNum, decEq, instDecidableEqZNum, decEq, instInhabitedNum, instInhabitedPosNum, instInhabitedZNum, instOneNum, instOnePosNum, instOneZNum, instReprNum, instReprPosNum, instReprZNum, instZeroNum, instZeroZNum, numNatCoe, posNumCoe, znumCoe	108
Theorems	0
Total	108

Num

Definitions

Name	Category	Theorems
add 📖	CompOp	—
bit 📖	CompOp	1 math math: bit_to_nat
bit0 📖	CompOp	4 math math: cast_bit0, bit0_of_bit0, ofNat'_bit, bit1_succ
bit1 📖	CompOp	4 math math: bit1_of_bit1, cast_bit1, ofNat'_bit, bit1_succ
cmp 📖	CompOp	4 math math: cmp_swap, cmp_eq, lt_iff_cmp, cmp_to_nat
decidableLE 📖	CompOp	—
decidableLT 📖	CompOp	—
div 📖	CompOp	—
div2 📖	CompOp	—
gcd 📖	CompOp	1 math math: gcd_to_nat
gcdAux 📖	CompOp	1 math math: gcd_to_nat_aux
instAdd 📖	CompOp	13 math math: bit1_of_bit1, add_zero, add_one, bit0_of_bit0, add_ofNat', PosNum.cast_to_num, ofNat'_succ, cast_add, add_toZNum, zero_add, add_of_nat, add_succ, add_to_nat
instDiv 📖	CompOp	2 math math: div_to_nat, div_zero
instLE 📖	CompOp	3 math math: cast_le, le_to_nat, le_iff_cmp
instLT 📖	CompOp	3 math math: cast_lt, lt_iff_cmp, lt_to_nat
instMod 📖	CompOp	3 math math: dvd_iff_mod_eq_zero, mod_to_nat, mod_zero
instMul 📖	CompOp	2 math math: cast_mul, mul_to_nat
instSub 📖	CompOp	1 math math: sub_to_nat
mul 📖	CompOp	—
natSize 📖	CompOp	2 math math: natSize_to_nat, size_eq_natSize
ofNat' 📖	CompOp	8 math math: ofNat'_one, of_to_nat', PosNum.of_to_nat', ofNat'_zero, add_ofNat', ofNat'_bit, ofNat'_succ, ofNat'_eq
ofZNum 📖	CompOp	2 math math: cast_ofZNum, ofZNum_toNat
ofZNum' 📖	CompOp	2 math math: mem_ofZNum', ofZNum'_toNat
ppred 📖	CompOp	1 math math: ppred_to_nat
pred 📖	CompOp	1 math math: pred_to_nat
psub 📖	CompOp	—
size 📖	CompOp	2 math math: size_to_nat, size_eq_natSize
sub 📖	CompOp	—
sub' 📖	CompOp	1 math math: cast_sub'
succ 📖	CompOp	7 math math: toZNumNeg_succ, add_one, cast_succ, succ_to_nat, bit1_succ, toZNum_succ, add_succ
succ' 📖	CompOp	4 math math: succ'_to_nat, PosNum.succ'_pred', cast_succ', PosNum.pred'_succ'
toZNum 📖	CompOp	11 math math: ZNum.abs_toZNum, toZNum_inj, zneg_toZNumNeg, ofInt'_toZNum, add_toZNum, mem_ofZNum', zneg_toZNum, ZNum.of_nat_toZNum, PosNum.sub'_one, toZNum_succ, cast_toZNum
toZNumNeg 📖	CompOp	6 math math: ZNum.of_nat_toZNumNeg, PosNum.one_sub', toZNumNeg_succ, zneg_toZNumNeg, zneg_toZNum, cast_toZNumNeg

PosNum

Definitions

Name	Category	Theorems
add 📖	CompOp	—
bit 📖	CompOp	1 math math: bit_to_nat
cmp 📖	CompOp	4 math math: cmp_swap, cmp_eq, cmp_to_nat, lt_iff_cmp
decidableLE 📖	CompOp	—
decidableLT 📖	CompOp	—
div' 📖	CompOp	1 math math: div'_to_nat
divMod 📖	CompOp	1 math math: divMod_to_nat
divModAux 📖	CompOp	1 math math: divMod_to_nat_aux
instAdd 📖	CompOp	7 math math: add_one, bit0_of_bit0, cast_add, add_succ, bit1_of_bit1, add_to_nat, one_add
instLE 📖	CompOp	3 math math: le_iff_cmp, cast_le, le_to_nat
instLT 📖	CompOp	3 math math: lt_to_nat, lt_iff_cmp, cast_lt
instMul 📖	CompOp	2 math math: cast_mul, mul_to_nat
instOfNatHAddNatOfNat 📖	CompOp	—
instSub 📖	CompOp	—
isOne 📖	CompOp	—
mod' 📖	CompOp	1 math math: mod'_to_nat
mul 📖	CompOp	—
natSize 📖	CompOp	3 math math: size_eq_natSize, natSize_pos, natSize_to_nat
ofNat 📖	CompOp	—
ofNatSucc 📖	CompOp	—
ofZNum 📖	CompOp	—
ofZNum' 📖	CompOp	—
pred 📖	CompOp	1 math math: pred_to_nat
pred' 📖	CompOp	7 math math: one_sub', pred'_to_nat, succ'_pred', to_int_eq_succ_pred, sub'_one, to_nat_eq_succ_pred, pred'_succ'
size 📖	CompOp	2 math math: size_to_nat, size_eq_natSize
sub 📖	CompOp	—
sub' 📖	CompOp	3 math math: one_sub', cast_sub', sub'_one
succ 📖	CompOp	5 math math: cast_succ, add_one, add_succ, succ_to_nat, one_add

ZNum

Definitions

Name	Category	Theorems
abs 📖	CompOp	2 math math: abs_toZNum, abs_to_nat
add 📖	CompOp	—
bit0 📖	CompOp	2 math math: bit0_of_bit0, cast_bit0
bit1 📖	CompOp	4 math math: zneg_bit1, cast_bit1, bit1_of_bit1, zneg_bitm1
bitm1 📖	CompOp	3 math math: zneg_bit1, cast_bitm1, zneg_bitm1
cmp 📖	CompOp	1 math math: cmp_to_int
decidableLE 📖	CompOp	—
decidableLT 📖	CompOp	—
div 📖	CompOp	—
gcd 📖	CompOp	1 math math: gcd_to_nat
instAdd 📖	CompOp	9 math math: cast_add, PosNum.cast_to_znum, bit0_of_bit0, Num.succ_ofInt', Num.add_toZNum, bit1_of_bit1, zero_add, add_zero, add_one
instDiv 📖	CompOp	2 math math: div_zero, div_to_int
instLE 📖	CompOp	3 math math: zeroLEOneClass, le_to_int, cast_le
instLT 📖	CompOp	2 math math: cast_lt, lt_to_int
instMod 📖	CompOp	2 math math: mod_to_int, dvd_iff_mod_eq_zero
instMul 📖	CompOp	2 math math: cast_mul, mul_to_int
instNeg 📖	CompOp	14 math math: neg_zero, zneg_succ, of_nat_toZNumNeg, cast_zneg, zneg_pos, neg_of_int, zneg_bit1, zneg_pred, Num.zneg_toZNumNeg, zneg_neg, Num.zneg_toZNum, ofInt'_neg, zneg_bitm1, zneg_zneg
mul 📖	CompOp	—
ofInt' 📖	CompOp	5 math math: Num.ofInt'_toZNum, Num.succ_ofInt', ofInt'_neg, of_to_int', ofInt'_eq
pred 📖	CompOp	4 math math: zneg_succ, Num.toZNumNeg_succ, zneg_pred, Num.pred_succ
succ 📖	CompOp	6 math math: zneg_succ, cast_succ, zneg_pred, Num.pred_succ, Num.toZNum_succ, add_one
zNeg 📖	CompOp	—

(root)

Definitions

Name	Category	Theorems
Num 📖	CompData	63 math math: Num.ofNat'_one, Num.cast_lt, Num.bit1_of_bit1, ZNum.of_nat_toZNumNeg, PosNum.land_eq_and, Num.div_to_nat, Num.sub_to_nat, Num.toNat_injective, Num.add_zero, Num.cast_le, PosNum.of_to_nat, Num.cast_zero, Num.castNum_shiftRight, Num.add_one, Num.castNum_xor, Num.to_of_nat, Num.castNum_shiftLeft, Num.of_to_nat, Num.isStrictOrderedRing, Num.lt_iff_cmp, Num.shiftr_eq_shiftRight, Num.bit0_of_bit0, Num.castNum_or, Num.shiftl_eq_shiftLeft, PosNum.shiftr_eq_shiftRight, Num.ofNat'_zero, Num.add_ofNat', Num.lxor_eq_xor, Num.castNum_and, PosNum.lxor_eq_xor, Num.lt_to_nat, Num.ppred_to_nat, PosNum.cast_to_num, Num.ofNat'_succ, Num.ofInt'_toZNum, Num.cast_add, Num.dvd_iff_mod_eq_zero, Num.cast_one, Num.dvd_to_nat, Num.add_toZNum, Num.zero_add, Num.add_of_nat, PosNum.divMod_to_nat_aux, Num.mem_ofZNum', PosNum.divMod_to_nat, ZNum.of_nat_toZNum, Num.cmp_to_nat, Num.ofZNum'_toNat, Num.land_eq_and, Num.le_to_nat, Num.cast_mul, Num.of_natCast, Num.mod_to_nat, Num.mod_zero, Num.ofNat'_eq, Num.mul_to_nat, Num.add_succ, Num.of_nat_inj, Num.isOrderedCancelAddMonoid, Num.div_zero, Num.le_iff_cmp, Num.add_to_nat, Num.lor_eq_or
PosNum 📖	CompData	26 math math: PosNum.shiftl_eq_shiftLeft, PosNum.land_eq_and, PosNum.one_sub', PosNum.cast_mul, PosNum.cast_one, PosNum.add_one, PosNum.shiftr_eq_shiftRight, PosNum.bit0_of_bit0, PosNum.cast_add, PosNum.add_succ, PosNum.lxor_eq_xor, PosNum.lt_to_nat, PosNum.le_iff_cmp, PosNum.cast_le, PosNum.le_to_nat, PosNum.lor_eq_or, PosNum.bit1_of_bit1, PosNum.mul_to_nat, PosNum.add_to_nat, PosNum.shiftl_succ_eq_bit0_shiftl, PosNum.cmp_to_nat, PosNum.lt_iff_cmp, PosNum.dvd_to_nat, PosNum.sub'_one, PosNum.cast_lt, PosNum.one_add
castNum 📖	CompOp	64 math math: Num.cast_to_int, Num.minFac_to_nat, Num.cast_lt, Num.gcd_to_nat_aux, Num.of_to_nat', Num.div_to_nat, Num.sub_to_nat, Num.succ'_to_nat, Num.toNat_injective, Num.castNum_eq_bitwise, Num.cast_le, ZNum.gcd_to_nat, Num.cast_bit0, Num.cast_zero', Num.cast_zero, Num.castNum_shiftRight, Num.size_to_nat, Num.castNum_xor, Num.to_of_nat, Num.castNum_shiftLeft, Num.of_to_nat, PosNum.pred'_to_nat, Num.cast_bit1, Num.castNum_or, Num.cast_succ, Num.cast_to_nat, Num.castNum_ldiff, Num.cast_sub', Num.cast_ofZNum, Num.succ_to_nat, PosNum.to_int_eq_succ_pred, PosNum.div'_to_nat, Num.castNum_and, Num.ofZNum_toNat, Num.lt_to_nat, Num.ppred_to_nat, Num.bit_to_nat, PosNum.mod'_to_nat, Num.cast_succ', Num.cast_add, Num.cast_inj, ZNum.abs_to_nat, Num.cast_one, Num.dvd_to_nat, PosNum.divMod_to_nat, Num.cmp_to_nat, Num.to_nat_to_int, Num.ofZNum'_toNat, Num.natSize_to_nat, Num.le_to_nat, Num.cast_mul, Num.of_natCast, Num.mod_to_nat, Num.to_nat_inj, Num.gcd_to_nat, Num.castNum_testBit, Num.size_eq_natSize, Num.mul_to_nat, PosNum.to_nat_eq_succ_pred, Num.pred_to_nat, Num.cast_toZNumNeg, Num.cast_pos, Num.cast_toZNum, Num.add_to_nat
castPosNum 📖	CompOp	47 math math: Num.minFac_to_nat, PosNum.pred_to_nat, PosNum.cast_bit1, Num.succ'_to_nat, ZNum.cast_neg, PosNum.of_to_nat, PosNum.size_to_nat, PosNum.cast_mul, PosNum.cast_one, PosNum.size_eq_natSize, PosNum.to_nat_pos, PosNum.cast_succ, PosNum.pred'_to_nat, PosNum.of_to_nat', PosNum.bit_to_nat, PosNum.cast_to_int, PosNum.to_nat_inj, PosNum.cast_to_znum, PosNum.cast_add, PosNum.to_int_eq_succ_pred, PosNum.natSize_to_nat, PosNum.div'_to_nat, PosNum.lt_to_nat, PosNum.cast_le, PosNum.le_to_nat, PosNum.cast_to_nat, PosNum.cast_one', PosNum.cast_to_num, PosNum.mod'_to_nat, Num.cast_succ', PosNum.mul_to_nat, PosNum.add_to_nat, PosNum.cast_pos, PosNum.cmp_to_nat, PosNum.divMod_to_nat, ZNum.cast_pos, PosNum.cast_bit0, PosNum.one_le_cast, PosNum.cast_inj, PosNum.cast_sub', PosNum.dvd_to_nat, PosNum.to_nat_to_int, PosNum.to_nat_eq_succ_pred, PosNum.cast_lt, PosNum.succ_to_nat, Num.cast_pos, PosNum.minFac_to_nat
castZNum 📖	CompOp	39 math math: ZNum.cast_zneg, ZNum.of_natCast, ZNum.cast_neg, ZNum.gcd_to_nat, ZNum.cmp_to_int, ZNum.of_intCast, ZNum.cast_succ, ZNum.mod_to_int, ZNum.cast_add, ZNum.cast_lt, ZNum.le_to_int, ZNum.cast_one, Num.cast_sub', Num.cast_ofZNum, ZNum.cast_inj, ZNum.cast_le, Num.ofZNum_toNat, ZNum.cast_zero', ZNum.cast_bit0, ZNum.cast_bitm1, ZNum.abs_to_nat, ZNum.to_of_int, ZNum.cast_zero, ZNum.of_to_int, ZNum.cast_bit1, ZNum.cast_mul, ZNum.div_to_int, ZNum.lt_to_int, ZNum.cast_pos, Num.ofZNum'_toNat, ZNum.cast_to_int, PosNum.cast_sub', ZNum.dvd_to_int, ZNum.cast_sub, ZNum.to_int_inj, ZNum.mul_to_int, Num.cast_toZNumNeg, ZNum.of_to_int', Num.cast_toZNum
instDecidableEqNum 📖	CompOp	—
instDecidableEqPosNum 📖	CompOp	—
instDecidableEqZNum 📖	CompOp	—
instInhabitedNum 📖	CompOp	—
instInhabitedPosNum 📖	CompOp	—
instInhabitedZNum 📖	CompOp	—
instOneNum 📖	CompOp	6 math math: Num.ofNat'_one, Num.bit1_of_bit1, Num.add_one, PosNum.cast_to_num, Num.ofNat'_succ, Num.cast_one
instOnePosNum 📖	CompOp	6 math math: PosNum.one_sub', PosNum.cast_one, PosNum.add_one, PosNum.bit1_of_bit1, PosNum.sub'_one, PosNum.one_add
instOneZNum 📖	CompOp	6 math math: ZNum.zeroLEOneClass, ZNum.cast_one, PosNum.cast_to_znum, Num.succ_ofInt', ZNum.bit1_of_bit1, ZNum.add_one
instReprNum 📖	CompOp	—
instReprPosNum 📖	CompOp	—
instReprZNum 📖	CompOp	—
instZeroNum 📖	CompOp	7 math math: Num.add_zero, Num.cast_zero, Num.ofNat'_zero, Num.dvd_iff_mod_eq_zero, Num.zero_add, Num.mod_zero, Num.div_zero
instZeroZNum 📖	CompOp	7 math math: ZNum.neg_zero, ZNum.zeroLEOneClass, ZNum.cast_zero, ZNum.dvd_iff_mod_eq_zero, ZNum.div_zero, ZNum.zero_add, ZNum.add_zero
numNatCoe 📖	CompOp	—
posNumCoe 📖	CompOp	—
znumCoe 📖	CompOp	—

instDecidableEqNum

Definitions

Name	Category	Theorems
decEq 📖	CompOp	—

instDecidableEqPosNum

Definitions

Name	Category	Theorems
decEq 📖	CompOp	—

instDecidableEqZNum

Definitions

Name	Category	Theorems
decEq 📖	CompOp	—

---

← Back to Index