Documentation Verification Report

ChineseRemainder

📁 Source: Mathlib/Data/Nat/ChineseRemainder.lean

Statistics

Metric	Count
Definitions `chineseRemainderOfFinset`, `chineseRemainderOfList`, `chineseRemainderOfMultiset`	3
Theorems `chineseRemainderOfFinset_lt_prod`, `chineseRemainderOfList_lt_prod`, `chineseRemainderOfList_modEq_unique`, `chineseRemainderOfList_nil`, `chineseRemainderOfList_perm`, `chineseRemainderOfMultiset_lt_prod`, `modEq_list_map_prod_iff`, `modEq_list_prod_iff`	8
Total	11

Nat

Definitions

Name	Category	Theorems
`chineseRemainderOfFinset` 📖	CompOp	1 math math: `chineseRemainderOfFinset_lt_prod`
`chineseRemainderOfList` 📖	CompOp	4 math math: `chineseRemainderOfList_nil`, `chineseRemainderOfList_modEq_unique`, `chineseRemainderOfList_lt_prod`, `chineseRemainderOfList_perm`
`chineseRemainderOfMultiset` 📖	CompOp	1 math math: `chineseRemainderOfMultiset_lt_prod`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`chineseRemainderOfFinset_lt_prod` 📖	mathematical	`Set.Pairwise` `SetLike.coe` `Finset` `Finset.instSetLike` `Function.onFun`	`chineseRemainderOfFinset` `Finset.prod` `instCommMonoid`	—	`chineseRemainderOfMultiset_lt_prod` `Finset.nodup`
`chineseRemainderOfList_lt_prod` 📖	mathematical	`Function.onFun`	`chineseRemainderOfList` `instOne`	—	`chineseRemainder_lt_mul` `instNontrivial` `IsDomain.to_noZeroDivisors` `instIsDomain`
`chineseRemainderOfList_modEq_unique` 📖	mathematical	`Function.onFun` `ModEq`	`instOne` `chineseRemainderOfList`	—	`chineseRemainder_modEq_unique`
`chineseRemainderOfList_nil` 📖	mathematical	—	`chineseRemainderOfList` `Function.onFun`	—	—
`chineseRemainderOfList_perm` 📖	mathematical	`Function.onFun`	`chineseRemainderOfList`	—	`List.Perm.prod_eq` `ModEq.eq_of_lt_of_lt` `ModEq.symm` `chineseRemainderOfList_modEq_unique` `Subtype.prop` `chineseRemainderOfList_lt_prod`
`chineseRemainderOfMultiset_lt_prod` 📖	mathematical	`Multiset.Nodup` `Set.Pairwise` `setOf` `Multiset` `Multiset.instMembership` `Function.onFun`	`chineseRemainderOfMultiset` `Multiset.prod` `instCommMonoid` `Multiset.map`	—	`chineseRemainderOfList_lt_prod` `List.Nodup.pairwise_of_forall_ne`
`modEq_list_map_prod_iff` 📖	mathematical	`Function.onFun`	`ModEq` `instOne`	—	`instIsEmptyFalse` `modEq_and_modEq_iff_modEq_mul`
`modEq_list_prod_iff` 📖	mathematical	—	`ModEq` `instOne`	—	`Fin.isEmpty'` `coprime_list_prod_right_iff` `modEq_and_modEq_iff_modEq_mul`

---

← Back to Index