Mathlib Map

Theorems · Theorem · number theory

threeGPFree_smul_set

∀ {α : Type u_2} [inst : CommMonoid α] [IsCancelMul α] {s : Set α} {a : α}, ThreeGPFree (a • s) ↔ ThreeGPFree s
Defined in
Mathlib.Combinatorics.Additive.AP.Three.Defs
Cited by
1 results in Mathlib
Foundations
Depth 11 from the axioms · uses propext
Assumes
CommMonoidIsCancelMul
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

mulRothNumber_map_mul_left · cited by 1mulRothNumber_map_mul_leftSet · cited by 53352SetCommMonoid · cited by 2264CommMonoidSet.smulSet · cited by 608Set.smulSetSet.mem_image_of_mem · cited by 371Set.mem_image_of_memsmul_eq_mul · cited by 357smul_eq_mulmul_mul_mul_comm · cited by 65mul_mul_mul_commIsCancelMul · cited by 32IsCancelMulThreeGPFree · cited by 29ThreeGPFreemul_left_cancel · cited by 16mul_left_cancelThreeGPFree.smul_set · cited by 2ThreeGPFree.smul_setthreeGPFree_smul_setCITED BYCITES

Cites10

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

Cited by1

Results whose statement or proof uses this declaration.