Mathlib Map

Theorems · Definition · number theory

ThreeGPFree

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

A set is 3GP-free if it does not contain any non-trivial geometric progression of length three.

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

Around this declaration

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

mulRothNumber · cited by 13mulRothNumbermulRothNumber_spec · cited by 6mulRothNumber_specThreeGPFree.le_mulRothNumber · cited by 6ThreeGPFree.le_mulRothNum…ThreeGPFree.mono · cited by 4ThreeGPFree.monoThreeGPFree.smul_set · cited by 2ThreeGPFree.smul_setthreeGPFree_image · cited by 2threeGPFree_imageThreeGPFree.smul_set₀ · cited by 1ThreeGPFree.smul_set₀IsMulFreimanIso.threeGPFree_congr · cited by 1IsMulFreimanIso.threeGPFr…mulRothNumber_map_mul_left · cited by 1mulRothNumber_map_mul_leftSet.Subsingleton.threeGPFree · cited by 1Subsingleton.threeGPFreethreeGPFree_empty · cited by 1threeGPFree_emptythreeGPFree_insert · cited by 1threeGPFree_insertthreeGPFree_singleton · cited by 1threeGPFree_singletonthreeGPFree_smul_set · cited by 1threeGPFree_smul_setIsMulFreimanHom.mulRothNumber_mono · cited by 1IsMulFreimanHom.mulRothNu…Set · cited by 53352SetMonoid · cited by 3887MonoidThreeGPFreeCITED 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
  • Monoidstatement and proof · cited by 3,887

Cited by30

Results whose statement or proof uses this declaration.