Sum-free sets

Sets with no solution to x+y=z or similar: sum-free sets in abelian groups and intervals, counts of sum-free and maximal sum-free sets, large sum-free subsets, square-sum-free, divisor-sum-free and non-averaging sets.

DefinitionProduct-free set#✓fully proved

A set \(S\) in a type \(M\) with a multiplication is product-free if \(xy \notin S\) for all \(x, y \in S\), where \(x\) and \(y\) need not be distinct.

def IsProductFree (S : Set M) : Prop :=
  ∀ x ∈ S, ∀ y ∈ S, x * y ∉ S

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.