Div

📁 Source: Mathlib/Data/Nat/Digits/Div.lean

Statistics

Metric	Count
Definitions	0
Theorems dvd_iff_dvd_digits_sum, dvd_iff_dvd_ofDigits, eleven_dvd_iff, eleven_dvd_of_palindrome, modEq_eleven_digits_sum, modEq_nine_digits_sum, modEq_three_digits_sum, nine_dvd_iff, three_dvd_iff	9
Total	9

Nat

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
dvd_iff_dvd_digits_sum 📖	mathematical	—	MulZeroClass.toZero instMulZeroClass digits	—	ofDigits_one ofDigits_digits ofDigits_mod
dvd_iff_dvd_ofDigits 📖	mathematical	—	ofDigits Int.instSemiring digits	—	dvd_iff_dvd_of_dvd_sub Int.ModEq.dvd Int.ModEq.symm zmodeq_ofDigits_digits Int.modEq_iff_dvd
eleven_dvd_iff 📖	mathematical	—	List.alternatingSum MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Int.instCommRing digits	—	dvd_iff_dvd_ofDigits instAtLeastTwoHAddOfNat sub_neg_eq_add ofDigits_neg_one
eleven_dvd_of_palindrome 📖	—	List.Palindrome digits Even	—	—	eleven_dvd_iff List.alternatingSum_reverse eq_zero_of_neg_eq Int.instIsOrderedAddMonoid neg_one_zsmul mul_one Even.neg_one_pow pow_succ' List.Palindrome.reverse_eq List.Palindrome.map
modEq_eleven_digits_sum 📖	mathematical	—	Int.ModEq List.alternatingSum MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Int.instCommRing digits	—	zmodeq_ofDigits_digits ofDigits_neg_one
modEq_nine_digits_sum 📖	mathematical	—	ModEq MulZeroClass.toZero instMulZeroClass digits	—	modEq_digits_sum
modEq_three_digits_sum 📖	mathematical	—	ModEq MulZeroClass.toZero instMulZeroClass digits	—	modEq_digits_sum
nine_dvd_iff 📖	mathematical	—	MulZeroClass.toZero instMulZeroClass digits	—	dvd_iff_dvd_digits_sum
three_dvd_iff 📖	mathematical	—	MulZeroClass.toZero instMulZeroClass digits	—	dvd_iff_dvd_digits_sum

---

← Back to Index