Theorems · Inductive type · number theory
IsApproximateAddSubgroup
{G : Type u_2} → [AddGroup G] → ℝ → Set G → PropAn approximate subgroup in a group is a symmetric set A containing the identity and such that
A + A can be covered by a small number of translates of A.
In practice, we will take K fixed and A large but finite.
- Cited by
- 14 results in Mathlib
- Foundations
- Depth 1 from the axioms · uses no axioms
- Assumes
- AddGroup
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites3
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
Cited by16
Results whose statement or proof uses this declaration.
- IsApproximateAddSubgroup.two_nsmul_covByVAddstatement and proof · cited by 6
- IsApproximateAddSubgroup.neg_eq_selfstatement and proof · cited by 5
- IsApproximateAddSubgroup.zero_memstatement and proof · cited by 5
- IsApproximateAddSubgroup.nonemptystatement and proof · cited by 3
- IsApproximateAddSubgroup.addSubgroupstatement · cited by 1
- IsApproximateAddSubgroup.card_nsmul_lestatement and proof · cited by 1
- IsApproximateAddSubgroup.nsmul_inter_nsmul_covByVAdd_sq_inter_sqstatement and proof · cited by 1
- IsApproximateAddSubgroup.one_lestatement and proof · cited by 1
- IsApproximateAddSubgroup.card_add_self_lestatement and proof · cited by 0
- IsApproximateAddSubgroup.casesOnstatement and proof · cited by 0
- IsApproximateAddSubgroup.imagestatement and proof · cited by 0
- IsApproximateAddSubgroup.monostatement and proof · cited by 0