Snevily's conjecture on Latin transversals

DefinitionSnevily's conjecture#✓fully proved

The statement that for every finite abelian group \(G\) of odd order, written additively, and all subsets \(A, B \subseteq G\) with \(|A| = |B|\), there is a bijection \(f \colon A \to B\) such that the sums \(a + f(a)\), for \(a \in A\), are pairwise distinct.

Equivalently, \(A\) and \(B\) can be enumerated as \(a_1, \dots, a_k\) and \(b_1, \dots, b_k\) so that the sums \(a_i + b_i\) are pairwise distinct: given such enumerations, send \(a_i\) to \(b_i\); conversely, enumerate \(A\) and transport the enumeration along \(f\).

def conjecture : Prop :=
  ∀ (G : Type) [AddCommGroup G] [Fintype G],
    Odd (Fintype.card G) →
      ∀ A B : Finset G, A.card = B.card →
        ∃ f : ↥A → ↥B, Function.Bijective f ∧
          ∀ a₁ a₂ : ↥A,
            (a₁ : G) + (f a₁ : G) = (a₂ : G) + (f a₂ : G) → a₁ = a₂

Sources

• OPG-655.

Used by 1

Used bySnevily's conjecture is true

TheoremSnevily's conjecture is true#●ready to prove

Let \(G\) be a finite abelian group of odd order, written additively, and let \(A, B \subseteq G\) be subsets with \(|A| = |B|\). Then there is a bijection \(f \colon A \to B\) such that the sums \(a + f(a)\), for \(a \in A\), are pairwise distinct.

public theorem_wanted conjecture_holds : conjecture

Sources

• Boris Arsovski, A proof of Snevily's conjecture, Israel J. Math. 182 (2011), 505-508.

Uses 1

Statement usesSnevily's conjecture

1 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.