English
If G is a cancellative semigroup and every nonempty Finset A has an a1,a2 in A with UniqueMul A A a1 a2, then UniqueProds G holds.
Русский
Если G — полугруппа с отменой и для каждого непустого конечного множества A существует пара a1,a2 ∈ A с UniqueMul A A a1 a2, то выполняется UniqueProds G.
LaTeX
$$$ \\forall G\\,[\\text{Semigroup }G][\\text{IsCancelMul }G],\\ h: \\forall \\{A\\: Finset G\}, A.Nonempty \\Rightarrow \\exists a_1\\in A,\\exists a_2\\in A, \\mathrm{UniqueMul} A A a_1 a_2 \\Rightarrow \\mathrm{UniqueProds }G.$$$
Lean4
/-- `UniqueProds G` says that for any two nonempty `Finset`s `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. -/
@[to_additive]
theorem of_same {G} [Semigroup G] [IsCancelMul G]
(h : ∀ {A : Finset G}, A.Nonempty → ∃ a1 ∈ A, ∃ a2 ∈ A, UniqueMul A A a1 a2) : UniqueProds G where
uniqueMul_of_nonempty {A B} hA
hB := by
classical
obtain ⟨g1, h1, g2, h2, hu⟩ := h (hB.mul hA)
obtain ⟨b1, hb1, a1, ha1, rfl⟩ := mem_mul.mp h1
obtain ⟨b2, hb2, a2, ha2, rfl⟩ := mem_mul.mp h2
refine ⟨a1, ha1, b2, hb2, fun a b ha hb he => ?_⟩
specialize hu (mul_mem_mul hb1 ha) (mul_mem_mul hb ha2) _
· rw [mul_assoc b1, ← mul_assoc a, he, mul_assoc a1, ← mul_assoc b1]
exact ⟨mul_left_cancel hu.1, mul_right_cancel hu.2⟩
