Documentation Verification Report

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`	`instHasSubset` `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`	`instHasSubset` `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`	`instHasSubset` `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`	`instHasSubset` `div` `DivInvMonoid.toDiv` `Finite`	—	`CanLift.prf` `instCanLiftFinsetCoeFinite` `Finset.ruzsa_covering_mul` `Nat.card_eq_fintype_card` `Fintype.card_coe` `instIsConcreteLE`

---

← Back to Index