English
If UniqueMul A B a0 b0 holds, then any two distinct representations (a,b) ≠ (a0,b0) give different products: a*b ≠ a0*b0.
Русский
Если UniqueMul A B a0 b0 выполняется, то любые две различные пары (a,b) и (a0,b0) дают различные произведения: a*b ≠ a0*b0.
LaTeX
$$$\\forall a\\in A\\,\\forall b\\in B\\, (a,b)\\neq (a_0,b_0) \\Rightarrow a b \\neq a_0 b_0$$$
Lean4
/-- Let `G` be a Type with multiplication, let `A B : Finset G` be finite subsets and
let `a0 b0 : G` be two elements. `UniqueMul A B a0 b0` asserts `a0 * b0` can be written in at
most one way as a product of an element of `A` and an element of `B`. -/
@[to_additive /-- Let `G` be a Type with addition, let `A B : Finset G` be finite subsets and
let `a0 b0 : G` be two elements. `UniqueAdd A B a0 b0` asserts `a0 + b0` can be written in at
most one way as a sum of an element from `A` and an element from `B`. -/
]
def UniqueMul {G} [Mul G] (A B : Finset G) (a0 b0 : G) : Prop :=
∀ ⦃a b⦄, a ∈ A → b ∈ B → a * b = a0 * b0 → a = a0 ∧ b = b0
