Theorems · Theorem · group theory

UniqueProds.of_same

∀ {G : Type u_1} [inst : Semigroup G] [IsCancelMul G],
  (∀ {A : Finset G}, A.Nonempty → ∃ a1 ∈ A, ∃ a2 ∈ A, UniqueMul A A a1 a2) → UniqueProds G

UniqueProds G says that for any two nonempty Finsets A and B in G, A × B contains a unique pair with the UniqueMul property. Strojnowski showed that if G is a group, then we only need to check this when A = B. Here we generalize the result to cancellative semigroups. Non-cancellative counterexample: the AddMonoid {0,1} with 1+1=1.

Defined in

Mathlib.Algebra.Group.UniqueProds.Basic

Cited by

0 results in Mathlib

Foundations

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

Assumes

SemigroupIsCancelMul