DivMod

📁 Source: Mathlib/Tactic/NormNum/DivMod.lean

Statistics

Metric	Count
Definitions evalIntDiv, evalIntDvd, evalIntMod	3
Theorems isInt_dvd_false, isInt_dvd_true, isInt_ediv, isInt_ediv_neg, isInt_ediv_zero, isInt_emod, isInt_emod_neg, isInt_emod_zero, isNat_neg_of_isNegNat	9
Total	12

Mathlib.Meta.NormNum

Definitions

Name	Category	Theorems
evalIntDiv 📖	CompOp	—
evalIntDvd 📖	CompOp	—
evalIntMod 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isInt_dvd_false 📖	—	IsInt Int.instRing	—	—	—
isInt_dvd_true 📖	—	IsInt Int.instRing	—	—	—
isInt_ediv 📖	—	IsInt Int.instRing IsNat AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne	—	—	LT.lt.ne' LE.le.trans_lt IsStrictOrderedRing.toIsOrderedRing Int.instIsStrictOrderedRing Int.instAddLeftMono Int.instZeroLEOneClass Int.instCharZero zero_add
isInt_ediv_neg 📖	—	IsInt Int.instRing	—	—	IsInt.out
isInt_ediv_zero 📖	—	IsInt Int.instRing IsNat AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne	—	—	Nat.cast_zero
isInt_emod 📖	—	IsInt Int.instRing IsNat AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne	—	—	IsStrictOrderedRing.toIsOrderedRing Int.instIsStrictOrderedRing Int.instAddLeftMono Int.instZeroLEOneClass Int.instCharZero
isInt_emod_neg 📖	—	IsNat AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing	—	—	IsNat.out
isInt_emod_zero 📖	—	IsInt Int.instRing IsNat AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne	—	—	Nat.cast_zero
isNat_neg_of_isNegNat 📖	mathematical	IsInt Int.instRing	IsNat AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne	—	IsInt.out Int.cast_negOfNat neg_neg

---

← Back to Index