RuzsaCovering

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

Statistics

Metric	Count
Definitions	0
Theorems ruzsa_covering_add, ruzsa_covering_mul, ruzsa_covering_add, ruzsa_covering_mul	4
Total	4

Finset

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ruzsa_covering_add 📖	mathematical	Nonempty Real Real.instLE Real.instNatCast card Finset add AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid Real.instMul	Finset instHasSubset Real Real.instLE Real.instNatCast card add AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid sub SubNegMonoid.toSub	—	exists_maximal instIsTransLe filter_nonempty_iff empty_mem_powerset coe_empty Set.pairwiseDisjoint_empty mem_filter mem_powerset le_of_mul_le_mul_right MulPosStrictMono.toMulPosReflectLE IsStrictOrderedRing.toMulPosStrictMono Real.instIsStrictOrderedRing card_add_iff pairwiseDisjoint_vadd_iff AddLeftCancelSemigroup.toIsLeftCancelAdd Nat.cast_mul Nat.mono_cast IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Real.instZeroLEOneClass card_le_card add_subset_add subset_refl instReflSubset Nat.cast_pos' NeZero.one Real.instNontrivial Nonempty.card_pos subset_add_left Nonempty.zero_mem_sub Maximal.not_gt insert_subset_iff coe_insert Set.PairwiseDisjoint.insert ssubset_insert neg_vadd_mem_iff not_disjoint_iff Mathlib.Tactic.Push.not_forall_eq mem_add mem_sub add_sub_add_right_eq_sub sub_neg_eq_add add_neg_cancel_left
ruzsa_covering_mul 📖	mathematical	Nonempty Real Real.instLE Real.instNatCast card Finset mul MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid Real.instMul	Finset instHasSubset Real Real.instLE Real.instNatCast card mul MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid div DivInvMonoid.toDiv	—	exists_maximal instIsTransLe filter_nonempty_iff empty_mem_powerset coe_empty le_of_mul_le_mul_right MulPosStrictMono.toMulPosReflectLE IsStrictOrderedRing.toMulPosStrictMono Real.instIsStrictOrderedRing card_mul_iff pairwiseDisjoint_smul_iff LeftCancelSemigroup.toIsLeftCancelMul Nat.cast_mul Nat.mono_cast IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Real.instZeroLEOneClass card_le_card mul_subset_mul subset_refl instReflSubset Nat.cast_pos' NeZero.one Real.instNontrivial Nonempty.card_pos subset_mul_left Nonempty.one_mem_div Maximal.not_gt insert_subset_iff coe_insert Set.PairwiseDisjoint.insert ssubset_insert Mathlib.Tactic.Push.not_forall_eq mem_mul mem_div mul_div_mul_right_eq_div div_inv_eq_mul mul_inv_cancel_left

Set

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ruzsa_covering_add 📖	mathematical	Nonempty Real Real.instLE Real.instNatCast Nat.card Elem Set add AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid Real.instMul	Set instHasSubset Real Real.instLE Real.instNatCast Nat.card Elem add AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid sub SubNegMonoid.toSub Finite	—	CanLift.prf instCanLiftFinsetCoeFinite Finset.ruzsa_covering_add Finset.coe_add Nat.card_eq_fintype_card Fintype.card_coe SetLike.coe_subset_coe instIsConcreteLE Finset.coe_sub Finset.finite_toSet
ruzsa_covering_mul 📖	mathematical	Nonempty Real Real.instLE Real.instNatCast Nat.card Elem Set mul MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid Real.instMul	Set instHasSubset Real Real.instLE Real.instNatCast Nat.card Elem mul MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid div DivInvMonoid.toDiv Finite	—	CanLift.prf instCanLiftFinsetCoeFinite Finset.ruzsa_covering_mul Nat.card_eq_fintype_card Fintype.card_coe instIsConcreteLE

---

← Back to Index