Documentation Verification Report

CauchyDavenport

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

Statistics

Metric	Count
Definitions	0
Theorems `cauchy_davenport`, `cauchy_davenport_add_of_linearOrder_isCancelAdd`, `cauchy_davenport_minOrder_add`, `cauchy_davenport_minOrder_mul`, `cauchy_davenport_mul_of_linearOrder_isCancelMul`, `cauchy_davenport_of_isAddTorsionFree`, `cauchy_davenport_of_isMulTorsionFree`	7
Total	7

ZMod

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`cauchy_davenport` 📖	mathematical	`Nat.Prime` `Finset.Nonempty` `ZMod`	`Finset.card` `Finset` `Finset.add` `decidableEq` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `commRing`	—	`minOrder_of_prime` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid` `IsOrderedRing.toZeroLEOneClass` `cauchy_davenport_minOrder_add`

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`cauchy_davenport_add_of_linearOrder_isCancelAdd` 📖	mathematical	`Finset.Nonempty`	`Finset.card` `Finset` `Finset.add` `LinearOrder.toDecidableEq`	—	`Finset.eq_singleton_iff_unique_mem` `Finset.mem_inter` `Finset.add_mem_add` `Finset.max'_mem` `Finset.mem_singleton_self` `Finset.min'_mem` `Finset.mem_add` `Finset.mem_singleton` `IsCancelAdd.toIsRightCancelAdd` `LE.le.eq_of_not_lt` `Finset.le_max'` `LT.lt.not_ge` `add_lt_add_left` `IsRightCancelAdd.addRightStrictMono_of_addRightMono` `add_le_add_right` `Finset.min'_le` `Finset.card_singleton_add` `IsCancelAdd.toIsLeftCancelAdd` `Finset.card_add_singleton` `Finset.card_union_add_card_inter` `Finset.card_singleton` `Finset.card_mono` `Finset.union_subset` `Finset.add_subset_add_left` `Finset.singleton_subset_iff` `Finset.add_subset_add_right`
`cauchy_davenport_minOrder_add` 📖	mathematical	`Finset.Nonempty`	`ENat` `Preorder.toLE` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompletelyDistribLattice.toCompleteLattice` `CompleteLinearOrder.toCompletelyDistribLattice` `instCompleteLinearOrderENat` `SemilatticeInf.toMin` `Lattice.toSemilatticeInf` `ConditionallyCompleteLattice.toLattice` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `AddMonoid.minOrder` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `ENat.instNatCast` `Finset.card` `Finset` `Finset.add` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass`	—	`Set.WellFoundedOn.induction` `min_le_iff` `Nat.cast_le` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid` `IsOrderedRing.toZeroLEOneClass` `tsub_le_iff_right` `Nat.instOrderedSub` `lt_or_ge` `neg_add_rev` `Finset.card_neg` `add_comm` `Finset.Nonempty.neg` `Finset.Nonempty.exists_eq_singleton_or_nontrivial` `Finset.card_singleton_add` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `Finset.card_singleton` `le_refl` `Iff.not` `neg_add_eq_zero` `Finset.mem_inter` `Finset.mem_vadd_finset` `add_neg_cancel_left` `eq_or_ne` `AddSubgroup.forall_mem_zmultiples` `zsmul_induction_right` `neg_add_cancel` `Finset.coe_vadd_finset` `VAddCommClass.vadd_comm` `Set.vaddCommClass_set` `VAddCommClass.opposite_mid` `VAddAssocClass.left` `Set.vadd_mem_vadd_set` `op_vadd_eq_add` `AddOpposite.op_neg` `Set.mem_vadd_set_iff_neg_vadd_mem` `AddSemigroup.opposite_vaddCommClass` `LE.le.trans` `AddMonoid.minOrder_le_natCard` `AddSubgroup.zmultiples_ne_bot` `Set.Finite.subset` `Set.Finite.vadd_set` `Finset.finite_toSet` `WithTop.coe_le_coe` `LE.le.trans_eq` `Nat.card_mono` `Nat.card_eq_fintype_card` `Fintype.card_coe` `Finset.card_vadd_finset` `Finset.card_le_card_add_right` `AddRightCancelSemigroup.toIsRightCancelAdd` `Finset.card_lt_card` `Finset.inter_subset_left` `Finset.eq_of_superset_of_card_ge` `HasSubset.Subset.trans` `Finset.instIsTransSubset` `Finset.inter_subset_right` `Eq.le` `Finset.card_mono` `Finset.addETransformLeft.fst_add_snd_subset` `Finset.addETransformRight.fst_add_snd_subset` `Finset.disjoint_or_nonempty_inter` `le_imp_le_of_le_of_le` `add_le_add_left` `covariant_swap_add_of_covariant_add` `Nat.instIsOrderedAddMonoid` `Finset.card_union_of_disjoint` `Finset.card_le_card_add_left` `le_add_of_le_left` `Nat.instCanonicallyOrderedAdd` `le_or_lt_of_add_le_add` `IsRightCancelAdd.addRightStrictMono_of_addRightMono` `Eq.ge` `Finset.AddETransform.card` `LE.le.trans'` `Finset.Nonempty.mono` `Finset.inter_subset_union` `LT.lt.le`
`cauchy_davenport_minOrder_mul` 📖	mathematical	`Finset.Nonempty`	`ENat` `Preorder.toLE` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompletelyDistribLattice.toCompleteLattice` `CompleteLinearOrder.toCompletelyDistribLattice` `instCompleteLinearOrderENat` `SemilatticeInf.toMin` `Lattice.toSemilatticeInf` `ConditionallyCompleteLattice.toLattice` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `Monoid.minOrder` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `ENat.instNatCast` `Finset.card` `Finset` `Finset.mul` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass`	—	`Set.WellFoundedOn.induction` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid` `IsOrderedRing.toZeroLEOneClass` `Nat.instOrderedSub` `lt_or_ge` `Finset.card_inv` `add_comm` `Finset.Nonempty.inv` `Finset.Nonempty.exists_eq_singleton_or_nontrivial` `Finset.card_singleton_mul` `LeftCancelSemigroup.toIsLeftCancelMul` `Finset.card_singleton` `Iff.not` `inv_mul_eq_one` `Finset.mem_inter` `Finset.mem_smul_finset` `mul_inv_cancel_left` `eq_or_ne` `Subgroup.forall_mem_zpowers` `zpow_induction_right` `inv_mul_cancel` `Finset.coe_smul_finset` `SMulCommClass.smul_comm` `Set.smulCommClass_set` `SMulCommClass.opposite_mid` `IsScalarTower.left` `Set.smul_mem_smul_set` `op_smul_eq_mul` `MulOpposite.op_inv` `Set.mem_smul_set_iff_inv_smul_mem` `Semigroup.opposite_smulCommClass` `LE.le.trans` `Monoid.minOrder_le_natCard` `Subgroup.zpowers_ne_bot` `Set.Finite.subset` `Set.Finite.smul_set` `Finset.finite_toSet` `WithTop.coe_le_coe` `LE.le.trans_eq` `Nat.card_mono` `Nat.card_eq_fintype_card` `Fintype.card_coe` `Finset.card_smul_finset` `Finset.card_le_card_mul_right` `RightCancelSemigroup.toIsRightCancelMul` `Finset.card_lt_card` `Finset.inter_subset_left` `Finset.eq_of_superset_of_card_ge` `HasSubset.Subset.trans` `Finset.instIsTransSubset` `Finset.inter_subset_right` `Eq.le` `Finset.card_mono` `Finset.mulETransformLeft.fst_mul_snd_subset` `Finset.mulETransformRight.fst_mul_snd_subset` `Finset.disjoint_or_nonempty_inter` `le_imp_le_of_le_of_le` `add_le_add_left` `covariant_swap_add_of_covariant_add` `Nat.instIsOrderedAddMonoid` `le_refl` `Finset.card_union_of_disjoint` `Finset.card_le_card_mul_left` `le_add_of_le_left` `Nat.instCanonicallyOrderedAdd` `le_or_lt_of_add_le_add` `IsRightCancelAdd.addRightStrictMono_of_addRightMono` `AddRightCancelSemigroup.toIsRightCancelAdd` `Eq.ge` `Finset.MulETransform.card` `LE.le.trans'` `Finset.Nonempty.mono` `Finset.inter_subset_union` `LT.lt.le`
`cauchy_davenport_mul_of_linearOrder_isCancelMul` 📖	mathematical	`Finset.Nonempty`	`Finset.card` `Finset` `Finset.mul` `LinearOrder.toDecidableEq`	—	`Finset.eq_singleton_iff_unique_mem` `Finset.mem_inter` `Finset.mul_mem_mul` `Finset.max'_mem` `Finset.mem_singleton_self` `Finset.min'_mem` `IsCancelMul.toIsRightCancelMul` `LE.le.eq_of_not_lt` `Finset.le_max'` `LT.lt.not_ge` `mul_lt_mul_left` `IsRightCancelMul.mulRightStrictMono_of_mulRightMono` `mul_le_mul_right` `Finset.min'_le` `Finset.card_singleton_mul` `IsCancelMul.toIsLeftCancelMul` `Finset.card_mul_singleton` `Finset.card_union_add_card_inter` `Finset.card_singleton` `Finset.card_mono` `Finset.union_subset` `Finset.mul_subset_mul_left` `Finset.singleton_subset_iff` `Finset.mul_subset_mul_right`
`cauchy_davenport_of_isAddTorsionFree` 📖	mathematical	`Finset.Nonempty`	`Finset.card` `Finset` `Finset.add` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid`	—	`AddMonoid.minOrder_eq_top` `min_eq_right` `le_top` `Nat.cast_le` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid` `IsOrderedRing.toZeroLEOneClass` `cauchy_davenport_minOrder_add`
`cauchy_davenport_of_isMulTorsionFree` 📖	mathematical	`Finset.Nonempty`	`Finset.card` `Finset` `Finset.mul` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid`	—	`Monoid.minOrder_eq_top` `min_eq_right` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid` `IsOrderedRing.toZeroLEOneClass` `cauchy_davenport_minOrder_mul`

---

← Back to Index