Documentation Verification Report

ApproximateSubgroup

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

Statistics

Metric	Count
Definitions `IsApproximateAddSubgroup`, `IsApproximateSubgroup`	2
Theorems `addSubgroup`, `card_add_self_le`, `card_nsmul_le`, `image`, `mono`, `neg_eq_self`, `nonempty`, `nsmul_inter_nsmul`, `nsmul_inter_nsmul_covByVAdd_sq_inter_sq`, `of_small_tripling`, `one_le`, `two_nsmul_covByVAdd`, `zero_mem`, `card_mul_self_le`, `card_pow_le`, `image`, `inv_eq_self`, `mono`, `nonempty`, `of_small_tripling`, `one_le`, `one_mem`, `pow_inter_pow`, `pow_inter_pow_covBySMul_sq_inter_sq`, `sq_covBySMul`, `subgroup`, `isApproximateAddSubgroup_zero`, `isApproximateSubgroup_one`	28
Total	30

IsApproximateAddSubgroup

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`addSubgroup` 📖	mathematical	—	`IsApproximateAddSubgroup` `Real` `Real.instOne` `SetLike.coe`	—	`ZeroMemClass.zero_mem` `AddSubmonoidClass.toZeroMemClass` `AddSubgroupClass.toAddSubmonoidClass` `neg_coe_set` `AddSubgroupClass.toNegMemClass` `Finset.card_singleton` `Nat.cast_one` `le_refl` `coe_set_nsmul` `Nat.instAtLeastTwoHAddOfNat` `OfNat.ofNat_ne_zero` `Nat.instCharZero` `Finset.coe_singleton` `Set.singleton_add` `Set.image_congr` `zero_add` `Set.image_id'` `subset_refl` `Set.instReflSubset`
`card_add_self_le` 📖	mathematical	`IsApproximateAddSubgroup` `SetLike.coe` `Finset` `Finset.instSetLike`	`Real` `Real.instLE` `Real.instNatCast` `Finset.card` `Finset.add` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `Real.instMul`	—	`two_nsmul` `pow_one` `card_nsmul_le`
`card_nsmul_le` 📖	mathematical	`IsApproximateAddSubgroup` `SetLike.coe` `Finset` `Finset.instSetLike`	`Real` `Real.instLE` `Real.instNatCast` `Finset.card` `AddMonoid.toNatSMul` `Finset.addMonoid` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `Real.instMul` `Monoid.toNatPow` `Real.instMonoid`	—	`zero_nsmul` `Finset.card_zero` `Nat.cast_one` `zero_tsub` `Nat.instCanonicallyOrderedAdd` `Nat.instOrderedSub` `pow_zero` `one_mul` `Nat.one_le_cast` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `Real.instZeroLEOneClass` `IsStrictOrderedRing.toCharZero` `Real.instIsStrictOrderedRing` `Finset.one_le_card` `Finset.coe_nonempty` `nonempty` `one_nsmul` `tsub_self` `le_refl` `two_nsmul_covByVAdd` `Nat.mono_cast` `Finset.card_le_card` `Finset.coe_nsmul` `Finset.coe_add` `SetLike.coe_subset_coe` `instIsConcreteLE` `Set.nsmul_subset_nsmul_add_of_sq_subset_add` `Nat.cast_mul` `Nat.cast_le` `Finset.card_add_le` `mul_le_mul_of_nonneg_right` `IsOrderedRing.toMulPosMono` `Real.instIsOrderedRing` `Nat.cast_pow` `Finset.card_nsmul_le` `Nat.cast_nonneg'` `pow_le_pow_left₀` `IsOrderedRing.toPosMulMono`
`image` 📖	mathematical	`IsApproximateAddSubgroup`	`Set.image` `DFunLike.coe`	—	`zero_mem` `map_zero` `AddMonoidHomClass.toZeroHomClass` `Set.image_neg` `neg_eq_self` `two_nsmul_covByVAdd` `Nat.cast_le` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `Real.instZeroLEOneClass` `IsStrictOrderedRing.toCharZero` `Real.instIsStrictOrderedRing` `Finset.card_image_le` `Set.image_nsmul` `Finset.coe_image` `Set.image_add` `AddMonoidHomClass.toAddHomClass` `Set.image_mono`
`mono` 📖	—	`Real` `Real.instLE` `IsApproximateAddSubgroup`	—	—	`zero_mem` `neg_eq_self` `CovByVAdd.mono` `two_nsmul_covByVAdd`
`neg_eq_self` 📖	mathematical	`IsApproximateAddSubgroup`	`Set` `Set.neg` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid`	—	—
`nonempty` 📖	mathematical	`IsApproximateAddSubgroup`	`Set.Nonempty`	—	`zero_mem`
`nsmul_inter_nsmul` 📖	mathematical	`IsApproximateAddSubgroup`	`Real` `Real.instMul` `Monoid.toNatPow` `Real.instMonoid` `Set` `Set.instInter` `Set.NSMul` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid`	—	`Set.zero_mem_nsmul` `zero_mem` `Set.inter_neg` `neg_nsmul` `neg_eq_self` `CovByVAdd.subset` `Set.inter_nsmul_subset` `mul_nsmul'` `Set.inter_subset_inter` `Set.nsmul_subset_nsmul` `subset_refl` `Set.instReflSubset` `nsmul_inter_nsmul_covByVAdd_sq_inter_sq`
`nsmul_inter_nsmul_covByVAdd_sq_inter_sq` 📖	mathematical	`IsApproximateAddSubgroup`	`CovByVAdd` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddMonoid.toAddAction` `Real` `Real.instMul` `Monoid.toNatPow` `Real.instMonoid` `Set` `Set.instInter` `Set.NSMul` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoid.toNatSMul` `Set.addMonoid`	—	`two_nsmul_covByVAdd` `one_le` `Nat.cast_mul` `Nat.cast_le` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `Real.instZeroLEOneClass` `IsStrictOrderedRing.toCharZero` `Real.instIsStrictOrderedRing` `Finset.card_image₂_le` `mul_le_mul` `IsOrderedRing.toPosMulMono` `Real.instIsOrderedRing` `IsOrderedRing.toMulPosMono` `Nat.cast_pow` `Finset.card_nsmul_le` `Nat.cast_nonneg'` `pow_nonneg` `IsOrderedRing.toZeroLEOneClass` `pow_le_pow_left₀` `le_of_lt` `pow_pos` `IsStrictOrderedRing.toPosMulStrictMono` `IsStrictOrderedRing.toZeroLEOneClass` `lt_of_lt_of_le` `Mathlib.Meta.Positivity.pos_of_isNat` `Real.instNontrivial` `Mathlib.Meta.NormNum.isNat_ofNat` `Nat.cast_one` `Set.inter_subset_inter` `Set.nsmul_subset_nsmul_add_of_sq_subset_add` `Set.iUnion_vadd_set` `Set.iUnion₂_inter_iUnion₂` `Set.iUnion_congr_Prop` `Finset.coe_nsmul` `Finset.mem_coe` `Set.iUnion_mono''` `neg_eq_self` `two_nsmul` `Finset.coe_image₂` `vadd_eq_add` `Set.biUnion_image2` `Set.exists_vadd_inter_vadd_subset_vadd_neg_add_inter_neg_add`
`of_small_tripling` 📖	mathematical	`Finset` `Finset.instMembership` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid` `Finset.neg` `NegZeroClass.toNeg` `Real` `Real.instLE` `Real.instNatCast` `Finset.card` `AddMonoid.toNatSMul` `Finset.addMonoid` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `Real.instMul`	`IsApproximateAddSubgroup` `Monoid.toNatPow` `Real.instMonoid` `Set` `Set.addMonoid` `SetLike.coe` `Finset.instSetLike`	—	`two_nsmul` `zero_add` `Set.add_mem_add` `neg_nsmul` `Finset.coe_neg` `succ_nsmul` `Finset.small_nsmul_of_small_tripling` `Finset.ruzsa_covering_add` `Finset.coe_nsmul` `Finset.coe_vadd` `SetLike.coe_subset_coe` `instIsConcreteLE` `zero_nsmul` `add_assoc` `sub_eq_add_neg`
`one_le` 📖	mathematical	`IsApproximateAddSubgroup`	`Real` `Real.instLE` `Real.instOne`	—	`two_nsmul_covByVAdd` `le_imp_le_of_le_of_le` `le_refl` `Finset.coe_empty` `Set.empty_add` `Set.subset_empty_iff` `Set.nsmul_eq_empty` `Set.Nonempty.ne_empty` `nonempty` `Nat.instAtLeastTwoHAddOfNat` `OfNat.ofNat_ne_zero` `Nat.instCharZero` `Finset.not_nonempty_iff_eq_empty` `Nat.one_le_cast` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `Real.instZeroLEOneClass` `IsStrictOrderedRing.toCharZero` `Real.instIsStrictOrderedRing` `Finset.one_le_card`
`two_nsmul_covByVAdd` 📖	mathematical	`IsApproximateAddSubgroup`	`CovByVAdd` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddMonoid.toAddAction` `Set` `Set.NSMul` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid` `AddSemigroup.toAdd` `AddMonoid.toAddSemigroup`	—	—
`zero_mem` 📖	mathematical	`IsApproximateAddSubgroup`	`Set` `Set.instMembership` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid`	—	—

IsApproximateSubgroup

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`card_mul_self_le` 📖	mathematical	`IsApproximateSubgroup` `SetLike.coe` `Finset` `Finset.instSetLike`	`Real` `Real.instLE` `Real.instNatCast` `Finset.card` `Finset.mul` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `Real.instMul`	—	`sq` `pow_one` `card_pow_le`
`card_pow_le` 📖	mathematical	`IsApproximateSubgroup` `SetLike.coe` `Finset` `Finset.instSetLike`	`Real` `Real.instLE` `Real.instNatCast` `Finset.card` `Monoid.toNatPow` `Finset.monoid` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `Real.instMul` `Real.instMonoid`	—	`pow_zero` `Finset.card_one` `Nat.cast_one` `zero_tsub` `Nat.instCanonicallyOrderedAdd` `Nat.instOrderedSub` `one_mul` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `Real.instZeroLEOneClass` `IsStrictOrderedRing.toCharZero` `Real.instIsStrictOrderedRing` `nonempty` `pow_one` `tsub_self` `sq_covBySMul` `Nat.mono_cast` `Finset.card_le_card` `instIsConcreteLE` `Set.pow_subset_pow_mul_of_sq_subset_mul` `Finset.card_mul_le` `mul_le_mul_of_nonneg_right` `IsOrderedRing.toMulPosMono` `Real.instIsOrderedRing` `Finset.card_pow_le` `Nat.cast_nonneg'` `pow_le_pow_left₀` `IsOrderedRing.toPosMulMono`
`image` 📖	mathematical	`IsApproximateSubgroup`	`Set.image` `DFunLike.coe`	—	`one_mem` `map_one` `MonoidHomClass.toOneHomClass` `inv_eq_self` `sq_covBySMul` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `Real.instZeroLEOneClass` `IsStrictOrderedRing.toCharZero` `Real.instIsStrictOrderedRing` `Finset.card_image_le` `Finset.coe_image` `MonoidHomClass.toMulHomClass` `Set.image_mono`
`inv_eq_self` 📖	mathematical	`IsApproximateSubgroup`	`Set` `Set.inv` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid`	—	—
`mono` 📖	—	`Real` `Real.instLE` `IsApproximateSubgroup`	—	—	`one_mem` `inv_eq_self` `CovBySMul.mono` `sq_covBySMul`
`nonempty` 📖	mathematical	`IsApproximateSubgroup`	`Set.Nonempty`	—	`one_mem`
`of_small_tripling` 📖	mathematical	`Finset` `Finset.instMembership` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `Finset.inv` `InvOneClass.toInv` `Real` `Real.instLE` `Real.instNatCast` `Finset.card` `Monoid.toNatPow` `Finset.monoid` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `Real.instMul`	`IsApproximateSubgroup` `Real.instMonoid` `Set` `Set.monoid` `SetLike.coe` `Finset.instSetLike`	—	`sq` `one_mul` `Set.mul_mem_mul` `pow_succ` `Finset.small_pow_of_small_tripling` `Finset.ruzsa_covering_mul` `instIsConcreteLE` `pow_zero` `mul_assoc` `div_eq_mul_inv`
`one_le` 📖	mathematical	`IsApproximateSubgroup`	`Real` `Real.instLE` `Real.instOne`	—	`sq_covBySMul` `le_imp_le_of_le_of_le` `le_refl` `Finset.coe_empty` `Set.empty_mul` `Set.Nonempty.ne_empty` `nonempty` `Nat.instCharZero` `Nat.instAtLeastTwoHAddOfNat` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `Real.instZeroLEOneClass` `IsStrictOrderedRing.toCharZero` `Real.instIsStrictOrderedRing`
`one_mem` 📖	mathematical	`IsApproximateSubgroup`	`Set` `Set.instMembership` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid`	—	—
`pow_inter_pow` 📖	mathematical	`IsApproximateSubgroup`	`Real` `Real.instMul` `Monoid.toNatPow` `Real.instMonoid` `Set` `Set.instInter` `Set.NPow` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid`	—	`Set.one_mem_pow` `one_mem` `Set.inter_inv` `inv_eq_self` `CovBySMul.subset` `Set.inter_pow_subset` `pow_mul'` `Set.inter_subset_inter` `Set.pow_subset_pow` `subset_refl` `Set.instReflSubset` `pow_inter_pow_covBySMul_sq_inter_sq`
`pow_inter_pow_covBySMul_sq_inter_sq` 📖	mathematical	`IsApproximateSubgroup`	`CovBySMul` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `Monoid.toMulAction` `Real` `Real.instMul` `Monoid.toNatPow` `Real.instMonoid` `Set` `Set.instInter` `Set.NPow` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `Set.monoid`	—	`sq_covBySMul` `one_le` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `Real.instZeroLEOneClass` `IsStrictOrderedRing.toCharZero` `Real.instIsStrictOrderedRing` `Finset.card_image₂_le` `mul_le_mul` `IsOrderedRing.toPosMulMono` `Real.instIsOrderedRing` `IsOrderedRing.toMulPosMono` `Finset.card_pow_le` `Nat.cast_nonneg'` `pow_nonneg` `IsOrderedRing.toZeroLEOneClass` `pow_le_pow_left₀` `le_of_lt` `pow_pos` `IsStrictOrderedRing.toPosMulStrictMono` `IsStrictOrderedRing.toZeroLEOneClass` `lt_of_lt_of_le` `Mathlib.Meta.Positivity.pos_of_isNat` `Real.instNontrivial` `Mathlib.Meta.NormNum.isNat_ofNat` `Nat.cast_one` `Set.inter_subset_inter` `Set.pow_subset_pow_mul_of_sq_subset_mul` `Set.iUnion₂_inter_iUnion₂` `Set.iUnion_congr_Prop` `Set.iUnion_mono''` `inv_eq_self` `Finset.coe_image₂` `smul_eq_mul` `Set.iUnion_smul_set` `Set.biUnion_image2` `Set.exists_smul_inter_smul_subset_smul_inv_mul_inter_inv_mul`
`sq_covBySMul` 📖	mathematical	`IsApproximateSubgroup`	`CovBySMul` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `Monoid.toMulAction` `Set` `Monoid.toNatPow` `Set.monoid`	—	—
`subgroup` 📖	mathematical	—	`IsApproximateSubgroup` `Real` `Real.instOne` `SetLike.coe`	—	`OneMemClass.one_mem` `SubmonoidClass.toOneMemClass` `SubgroupClass.toSubmonoidClass` `inv_coe_set` `SubgroupClass.toInvMemClass` `Finset.card_singleton` `Nat.cast_one` `coe_set_pow` `Nat.instCharZero` `Nat.instAtLeastTwoHAddOfNat` `Finset.coe_singleton` `Set.singleton_mul` `Set.image_congr` `one_mul` `Set.image_id'` `Set.instReflSubset`

(root)

Definitions

Name	Category	Theorems
`IsApproximateAddSubgroup` 📖	CompData	3 math math: `isApproximateAddSubgroup_zero`, `IsApproximateAddSubgroup.addSubgroup`, `IsApproximateAddSubgroup.of_small_tripling`
`IsApproximateSubgroup` 📖	CompData	3 math math: `IsApproximateSubgroup.subgroup`, `IsApproximateSubgroup.of_small_tripling`, `isApproximateSubgroup_one`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isApproximateAddSubgroup_zero` 📖	mathematical	—	`IsApproximateAddSubgroup` `Real` `Real.instOne` `SetLike.coe` `AddSubgroup` `AddSubgroup.instSetLike`	—	`IsApproximateAddSubgroup.two_nsmul_covByVAdd` `Nat.cast_le_one` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `Real.instZeroLEOneClass` `IsStrictOrderedRing.toCharZero` `Real.instIsStrictOrderedRing` `Finset.card_le_one_iff_subset_singleton` `Zero.instNonempty` `Finset.subset_singleton_iff` `Finset.coe_empty` `Set.empty_add` `Set.subset_empty_iff` `Set.nsmul_eq_empty` `Set.Nonempty.ne_empty` `IsApproximateAddSubgroup.nonempty` `Nat.instAtLeastTwoHAddOfNat` `OfNat.ofNat_ne_zero` `Nat.instCharZero` `two_nsmul` `Set.singleton_vadd` `Finset.coe_singleton` `Set.subset_vadd_set_iff` `add_zero` `Set.vadd_mem_vadd_set` `Set.add_mem_add` `IsApproximateAddSubgroup.zero_mem` `IsApproximateAddSubgroup.neg_eq_self` `Set.mem_neg` `neg_add_rev` `vadd_vadd` `neg_add_cancel_left` `Set.vadd_set_mono` `Set.vadd_set_subset_vadd` `Set.neg_mem_neg` `IsApproximateAddSubgroup.addSubgroup` `AddSubgroup.instAddSubgroupClass`
`isApproximateSubgroup_one` 📖	mathematical	—	`IsApproximateSubgroup` `Real` `Real.instOne` `SetLike.coe` `Subgroup` `Subgroup.instSetLike`	—	`IsApproximateSubgroup.sq_covBySMul` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `Real.instZeroLEOneClass` `IsStrictOrderedRing.toCharZero` `Real.instIsStrictOrderedRing` `One.instNonempty` `Finset.coe_empty` `Set.empty_mul` `Set.Nonempty.ne_empty` `IsApproximateSubgroup.nonempty` `Nat.instCharZero` `Nat.instAtLeastTwoHAddOfNat` `sq` `Set.singleton_smul` `Finset.coe_singleton` `Set.subset_smul_set_iff` `mul_one` `Set.smul_mem_smul_set` `Set.mul_mem_mul` `IsApproximateSubgroup.one_mem` `IsApproximateSubgroup.inv_eq_self` `mul_inv_rev` `smul_smul` `inv_mul_cancel_left` `Set.smul_set_mono` `Set.smul_set_subset_smul` `Set.inv_mem_inv` `IsApproximateSubgroup.subgroup` `Subgroup.instSubgroupClass`

---

← Back to Index