Init

📁 Source: Mathlib/Data/Int/Init.lean

Statistics

Metric	Count
Definitions inductionOn', neg, pos, natMod, negInduction, pred, strongRec, succ	8
Theorems div_dvd_iff_dvd_mul, div_le_div_iff_of_dvd_of_neg_of_neg, div_le_div_iff_of_dvd_of_neg_of_pos, div_le_div_iff_of_dvd_of_pos_of_neg, div_le_div_iff_of_dvd_of_pos_of_pos, div_le_iff_of_dvd_of_neg, div_le_iff_of_dvd_of_pos, div_lt_div_iff_of_dvd_of_neg_of_neg, div_lt_div_iff_of_dvd_of_neg_of_pos, div_lt_div_iff_of_dvd_of_pos, div_lt_div_iff_of_dvd_of_pos_of_neg, div_lt_iff_of_dvd_of_neg, div_lt_iff_of_dvd_of_pos, dvd_div_iff_mul_dvd, dvd_div_of_mul_dvd, dvd_mul_of_div_dvd, ediv_of_neg_of_pos, emod_two_eq_zero_or_one, eq_mul_div_of_mul_eq_mul_of_dvd_left, exists_lt_and_lt_iff_not_dvd, ext_ediv_emod, ext_ediv_emod_iff, gcd_negSucc_negSucc, gcd_negSucc_ofNat, gcd_ofNat_negSucc, inductionOn'_self, inductionOn'_sub_one, induction_on, le_add_iff_lt_of_dvd_sub, le_div_iff_of_dvd_of_neg, le_div_iff_of_dvd_of_pos, le_iff_pos_of_dvd, le_induction, le_induction_down, lt_div_iff_of_dvd_of_neg, lt_div_iff_of_dvd_of_pos, lt_succ_self, mul_dvd_of_dvd_div, natAbs_sq, natCast_div, natCast_mod, natCast_pred_of_pos, natMod_lt, neg_eq_neg, neg_nat_succ, neg_pred, neg_succ, ofNat_add_negSucc_of_ge, pow_eq, pred_nat_succ, pred_neg_pred, pred_self_lt, pred_succ, sign_add_eq_of_sign_eq, sign_mul_self_eq_natAbs, strongRec_of_lt, succ_neg_natCast_succ, succ_neg_succ, succ_pred, toNat_lt_of_ne_zero, toNat_pred_coe_of_pos	61
Total	69

Int

Definitions

Name	Category	Theorems
inductionOn' 📖	CompOp	3 math math: inductionOn'_add_one, inductionOn'_self, inductionOn'_sub_one
natMod 📖	CompOp	2 math math: divModEquiv_apply, natMod_lt
negInduction 📖	CompOp	—
pred 📖	CompOp	9 math math: pred_self_lt, succ_pred, pred_succ, neg_pred, pred_nat_succ, pred_eq_pred, neg_nat_succ, pred_neg_pred, neg_succ
strongRec 📖	CompOp	2 math math: strongRec_of_lt, strongRec_of_ge
succ 📖	CompOp	9 math math: lt_succ_self, lt_succ_floor, succ_pred, pred_succ, succ_neg_natCast_succ, neg_pred, succ_neg_succ, succ_eq_succ, neg_succ

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
div_dvd_iff_dvd_mul 📖	—	—	—	—	—
div_le_div_iff_of_dvd_of_neg_of_neg 📖	—	—	—	—	—
div_le_div_iff_of_dvd_of_neg_of_pos 📖	—	—	—	—	—
div_le_div_iff_of_dvd_of_pos_of_neg 📖	—	—	—	—	—
div_le_div_iff_of_dvd_of_pos_of_pos 📖	—	—	—	—	—
div_le_iff_of_dvd_of_neg 📖	—	—	—	—	—
div_le_iff_of_dvd_of_pos 📖	—	—	—	—	—
div_lt_div_iff_of_dvd_of_neg_of_neg 📖	—	—	—	—	—
div_lt_div_iff_of_dvd_of_neg_of_pos 📖	—	—	—	—	—
div_lt_div_iff_of_dvd_of_pos 📖	—	—	—	—	—
div_lt_div_iff_of_dvd_of_pos_of_neg 📖	—	—	—	—	—
div_lt_iff_of_dvd_of_neg 📖	—	—	—	—	—
div_lt_iff_of_dvd_of_pos 📖	—	—	—	—	—
dvd_div_iff_mul_dvd 📖	—	—	—	—	—
dvd_div_of_mul_dvd 📖	—	—	—	—	—
dvd_mul_of_div_dvd 📖	—	—	—	—	—
ediv_of_neg_of_pos 📖	—	—	—	—	—
emod_two_eq_zero_or_one 📖	—	—	—	—	—
eq_mul_div_of_mul_eq_mul_of_dvd_left 📖	—	—	—	—	—
exists_lt_and_lt_iff_not_dvd 📖	—	—	—	—	—
ext_ediv_emod 📖	—	—	—	—	—
ext_ediv_emod_iff 📖	—	—	—	—	—
gcd_negSucc_negSucc 📖	—	—	—	—	—
gcd_negSucc_ofNat 📖	—	—	—	—	—
gcd_ofNat_negSucc 📖	—	—	—	—	—
inductionOn'_self 📖	mathematical	—	inductionOn'	—	—
inductionOn'_sub_one 📖	mathematical	—	inductionOn'	—	inductionOn'_self inductionOn'.eq_1
induction_on 📖	—	—	—	—	—
le_add_iff_lt_of_dvd_sub 📖	—	—	—	—	le_iff_pos_of_dvd
le_div_iff_of_dvd_of_neg 📖	—	—	—	—	—
le_div_iff_of_dvd_of_pos 📖	—	—	—	—	—
le_iff_pos_of_dvd 📖	—	—	—	—	—
le_induction 📖	—	—	—	—	—
le_induction_down 📖	—	—	—	—	—
lt_div_iff_of_dvd_of_neg 📖	—	—	—	—	—
lt_div_iff_of_dvd_of_pos 📖	—	—	—	—	—
lt_succ_self 📖	mathematical	—	succ	—	—
mul_dvd_of_dvd_div 📖	—	—	—	—	—
natAbs_sq 📖	—	—	—	—	—
natCast_div 📖	—	—	—	—	—
natCast_mod 📖	—	—	—	—	—
natCast_pred_of_pos 📖	—	—	—	—	—
natMod_lt 📖	mathematical	—	natMod	—	toNat_lt_of_ne_zero
neg_eq_neg 📖	—	—	—	—	—
neg_nat_succ 📖	mathematical	—	pred	—	neg_succ
neg_pred 📖	mathematical	—	pred succ	—	neg_succ
neg_succ 📖	mathematical	—	succ pred	—	—
ofNat_add_negSucc_of_ge 📖	—	—	—	—	—
pow_eq 📖	—	—	—	—	—
pred_nat_succ 📖	mathematical	—	pred	—	pred_succ
pred_neg_pred 📖	mathematical	—	pred	—	neg_pred pred_succ
pred_self_lt 📖	mathematical	—	pred	—	—
pred_succ 📖	mathematical	—	pred succ	—	—
sign_add_eq_of_sign_eq 📖	—	—	—	—	—
sign_mul_self_eq_natAbs 📖	—	—	—	—	—
strongRec_of_lt 📖	mathematical	—	strongRec	—	—
succ_neg_natCast_succ 📖	mathematical	—	succ	—	succ_neg_succ
succ_neg_succ 📖	mathematical	—	succ	—	neg_succ succ_pred
succ_pred 📖	mathematical	—	succ pred	—	—
toNat_lt_of_ne_zero 📖	—	—	—	—	—
toNat_pred_coe_of_pos 📖	—	—	—	—	natCast_pred_of_pos

Int.inductionOn'

Definitions

Name	Category	Theorems
neg 📖	CompOp	—
pos 📖	CompOp	—

---

← Back to Index