ErdosGinzburgZiv

📁 Source: Mathlib/Combinatorics/Additive/ErdosGinzburgZiv.lean

Statistics

Metric	Count
Definitions	0
Theorems erdos_ginzburg_ziv, erdos_ginzburg_ziv_multiset, erdos_ginzburg_ziv, erdos_ginzburg_ziv_multiset	4
Total	4

Int

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
erdos_ginzburg_ziv 📖	mathematical	Finset.card	Finset Finset.instHasSubset Finset.sum instAddCommMonoid	—	Nat.prime_composite_induction CharP.cast_eq_zero CharP.ofCharZero instCharZero Nat.cast_one mul_one Finset.exists_subset_card_eq HasSubset.Subset.trans Finset.instIsTransSubset Finset.coe_empty instIsEmptyFalse mul_le_mul_left covariant_swap_mul_of_covariant_mul Nat.instMulLeftMono tsub_mul Nat.instCanonicallyOrderedAdd Nat.instOrderedSub LE.total IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT AddLeftCancelSemigroup.toIsLeftCancelAdd contravariant_lt_of_covariant_le IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid mul_assoc tsub_right_comm Finset.sum_const_nat tsub_le_tsub Finset.card_biUnion_le Finset.le_card_sdiff Disjoint.mono Finset.subset_biUnion_of_mem Finset.sdiff_disjoint Finset.card_cons Finset.cons_eq_insert Finset.coe_insert Set.pairwise_insert_of_symmetric symmetric_disjoint Finset.sdiff_subset le_rfl Eq.ge Finset.biUnion_subset Finset.card_biUnion Set.Pairwise.mono Finset.sum_biUnion mul_comm dvd_div_iff_mul_dvd Finset.dvd_sum sum_div
erdos_ginzburg_ziv_multiset 📖	mathematical	Multiset.card	Multiset Preorder.toLE PartialOrder.toPreorder Multiset.instPartialOrder Multiset.sum instAddCommMonoid	—	erdos_ginzburg_ziv Multiset.card_toEnumFinset Nat.instOrderedSub Multiset.map_fst_le_of_subset_toEnumFinset Multiset.card_map

ZMod

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
erdos_ginzburg_ziv 📖	mathematical	Finset.card	Finset Finset.instHasSubset Finset.sum ZMod NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing commRing MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	—	Finset.sum_congr Int.cast_sum intCast_cast cast_id' Int.erdos_ginzburg_ziv
erdos_ginzburg_ziv_multiset 📖	mathematical	Multiset.card ZMod	Multiset Preorder.toLE PartialOrder.toPreorder Multiset.instPartialOrder Multiset.sum NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing commRing MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	—	erdos_ginzburg_ziv Multiset.card_toEnumFinset Nat.instOrderedSub Multiset.map_fst_le_of_subset_toEnumFinset Multiset.card_map

---

← Back to Index