Theorems · Theorem · group theory

TwoUniqueProds.uniqueMul_of_one_lt_card

∀ {G : Type u_1} {inst : Mul G} [self : TwoUniqueProds G] {A B : Finset G},
  1 < A.card * B.card → ∃ p1 ∈ A ×ˢ B, ∃ p2 ∈ A ×ˢ B, p1 ≠ p2 ∧ UniqueMul A B p1.1 p1.2 ∧ UniqueMul A B p2.1 p2.2

For A B two finite sets whose product has cardinality at least 2, we can find at least two unique pairs.

Defined in

Mathlib.Algebra.Group.UniqueProds.Basic

Cited by

2 results in Mathlib

Foundations

Depth 64 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

TwoUniqueProds