Mathlib Map

Theorems · Theorem · number theory

threeAPFree_vadd_set

∀ {α : Type u_2} [inst : AddCommMonoid α] [IsCancelAdd α] {s : Set α} {a : α}, ThreeAPFree (a +ᵥ s) ↔ ThreeAPFree s
Defined in
Mathlib.Combinatorics.Additive.AP.Three.Defs
Cited by
1 results in Mathlib
Foundations
Depth 10 from the axioms · uses propext
Assumes
AddCommMonoidIsCancelAdd
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

addRothNumber_map_add_left · cited by 3addRothNumber_map_add_leftSet · cited by 53352SetAddCommMonoid · cited by 12281AddCommMonoidHVAdd.hVAdd · cited by 1820HVAdd.hVAddSet.vaddSet · cited by 403Set.vaddSetSet.mem_image_of_mem · cited by 371Set.mem_image_of_memIsCancelAdd · cited by 79IsCancelAddadd_add_add_comm · cited by 56add_add_add_commvadd_eq_add · cited by 39vadd_eq_addThreeAPFree · cited by 38ThreeAPFreeadd_left_cancel · cited by 29add_left_cancelThreeAPFree.vadd_set · cited by 2ThreeAPFree.vadd_setthreeAPFree_vadd_setCITED BYCITES

Cites11

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.