Mathlib Map

Theorems · Definition · number theory

ThreeAPFree

{α : Type u_2} → [AddMonoid α] → Set α → Prop

A set is 3AP-free if it does not contain any non-trivial arithmetic progression of length three. This is also sometimes called a non-averaging set or Salem-Spencer set.

Defined in
Mathlib.Combinatorics.Additive.AP.Three.Defs
Cited by
38 results in Mathlib
Foundations
Depth 6 from the axioms · uses no axioms
Assumes
AddMonoid
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

addRothNumber · cited by 20addRothNumberaddRothNumber_spec · cited by 8addRothNumber_specThreeAPFree.le_addRothNumber · cited by 7ThreeAPFree.le_addRothNum…ThreeAPFree.mono · cited by 5ThreeAPFree.monoaddRothNumber_map_add_left · cited by 3addRothNumber_map_add_leftThreeAPFree.of_image · cited by 3ThreeAPFree.of_imagethreeAPFree_image · cited by 2threeAPFree_imagethreeAPFree_singleton · cited by 2threeAPFree_singletonIsAddFreimanHom.addRothNumber_mono · cited by 2IsAddFreimanHom.addRothNu…ThreeAPFree.vadd_set · cited by 2ThreeAPFree.vadd_setthreeAPFree_empty · cited by 1threeAPFree_emptySet.Subsingleton.threeAPFree · cited by 1Subsingleton.threeAPFreethreeAPFree_frontier · cited by 1threeAPFree_frontierthreeAPFree_insert · cited by 1threeAPFree_insertthreeAPFree_sphere · cited by 1threeAPFree_sphereSet · cited by 53352SetAddMonoid · cited by 2864AddMonoidThreeAPFreeCITED BYCITES

Cites2

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

  • Setstatement and proof · cited by 53,352
  • AddMonoidstatement and proof · cited by 2,864

Cited by39

Results whose statement or proof uses this declaration.