UniqueSums.addHom_image_iff
theorem UniqueSums.addHom_image_iff :
∀ {G : Type u} {H : Type v} [inst : Add G] [inst_1 : Add H], G ≃+ H → (UniqueSums G ↔ UniqueSums H)
This theorem states that the property `UniqueSums` is preserved under additive equivalences. It applies to any two types `G` and `H` that have an additive structure. More specifically, if there is an additive equivalence between `G` and `H`, then `G` has the `UniqueSums` property if and only if `H` also has the `UniqueSums` property. The `UniqueSums` property is about the uniqueness of the sum of elements in a set.
More concisely: If `G` and `H` have an additive structure and there is an additive equivalence between them, then `G` has the property of unique sums if and only if `H` does.
|
UniqueAdd.of_addOpposite
theorem UniqueAdd.of_addOpposite :
∀ {G : Type u_1} [inst : Add G] {A B : Finset G} {a0 b0 : G},
UniqueAdd (Finset.map { toFun := AddOpposite.op, inj' := ⋯ } B)
(Finset.map { toFun := AddOpposite.op, inj' := ⋯ } A) (AddOpposite.op b0) (AddOpposite.op a0) →
UniqueAdd A B a0 b0
This theorem states that for any type `G` with an addition operation, given two finite subsets `A` and `B` of `G` and two elements `a0` and `b0` from `G`, if the sum of an element from the image finset of `B` under the operation `AddOpposite.op` and an element from the image finset of `A` under the same operation, can be written in at most one way as `AddOpposite.op b0` plus `AddOpposite.op a0`, then it also holds that the sum `a0 + b0` can be written in at most one way as a sum of an element from `A` and an element from `B`. In other words, the uniqueness of addition in the opposite world implies the uniqueness of addition in the original world.
More concisely: If the sum of an element from the image of a finite set `A` under `AddOpposite.op` and an element from the image of another finite set `B` under `AddOpposite.op` can be written as `AddOpposite.op b0 + AddOpposite.op a0` for at most one pair `(a0, b0)`, then the sum `a0 + b0` can be written as `x + y` with `x ∈ A` and `y ∈ B` for at most one pair `(x, y)`.
|
UniqueProds.mulHom_image_iff
theorem UniqueProds.mulHom_image_iff :
∀ {G : Type u} {H : Type v} [inst : Mul G] [inst_1 : Mul H], G ≃* H → (UniqueProds G ↔ UniqueProds H)
The theorem `UniqueProds.mulHom_image_iff` states that for any two types `G` and `H` that have multiplication defined on them, if there exists a multiplicative equivalence between `G` and `H`, then the property of having unique products is preserved under this equivalence. In other words, `G` having unique products is equivalent to `H` having unique products. Unique products here mean that given any two elements, there is exactly one way to multiply them.
More concisely: If types `G` and `H` with multiplication have a multiplicative equivalence, then `G` having unique products is equivalent to `H` having unique products.
|
UniqueProds.uniqueMul_of_nonempty
theorem UniqueProds.uniqueMul_of_nonempty :
∀ {G : Type u_1} [inst : Mul G] [self : UniqueProds G] {A B : Finset G},
A.Nonempty → B.Nonempty → ∃ a0 ∈ A, ∃ b0 ∈ B, UniqueMul A B a0 b0
This theorem states that for two nonempty finite sets `A` and `B` in a type `G` with a multiplication operation, there always exist two elements `a0` and `b0` such that `a0` is in `A` and `b0` is in `B`, and their product `a0 * b0` can be expressed in at most one way as a product of an element of `A` and an element of `B`. This assertion is known as `UniqueMul A B a0 b0`. More formally, for every pair of elements `a` in `A` and `b` in `B`, if `a * b` equals `a0 * b0`, then `a` must equal `a0` and `b` must equal `b0`.
More concisely: Given two nonempty finite sets `A` and `B` in a group `G` with multiplication operation, there exists a unique pair `(a0, b0)` of elements, one in `A` and one in `B`, such that their product is the product of any other pair in `A × B`.
|
UniqueProds.of_same
theorem UniqueProds.of_same :
∀ {G : Type u_1} [inst : Semigroup G] [inst_1 : IsCancelMul G],
(∀ {A : Finset G}, A.Nonempty → ∃ a1 ∈ A, ∃ a2 ∈ A, UniqueMul A A a1 a2) → UniqueProds G
The theorem `UniqueProds.of_same` states the following: Given a type `G` that is a semigroup and has the cancellation property with respect to multiplication, if for any nonempty finite subset `A` of `G` there exist two elements `a1` and `a2` in `A` such that the product of `a1` and `a2` can be written in at most one way as a product of two elements of `A`, then `G` has the property that for any pair of nonempty subsets `A` and `B`, the Cartesian product `A × B` contains a unique pair with the `UniqueMul` property. This is a generalization of a result by Strojnowski that only required checking this property when `A = B` and `G` was a group. The theorem also mentions a counterexample showing that this property does not necessarily hold for non-cancellative semigroups, specifically the additive monoid {0,1} where 1+1=1.
More concisely: Given a cancellative semigroup `G` with the property that for any nonempty finite subsets `A` and `B` of `G`, there exists at most one pair of elements `(a, b)` in `A × B` such that `a × b` is the product of two elements from `A` and `B` respectively, then `G` has the unique product property for all pairs of nonempty subsets.
|
TwoUniqueProds.of_injective_mulHom
theorem TwoUniqueProds.of_injective_mulHom :
∀ {G : Type u} {H : Type v} [inst : Mul G] [inst_1 : Mul H] (f : H →ₙ* G),
Function.Injective ⇑f → TwoUniqueProds G → TwoUniqueProds H
The theorem `TwoUniqueProds.of_injective_mulHom` states that for any types `G` and `H` equipped with multiplication (`Mul G` and `Mul H`), given an injective group homomorphism `f` (a function preserving multiplication) from `H` to `G`, if `G` satisfies the `TwoUniqueProds` property, then `H` also satisfies the `TwoUniqueProds` property. Here, the `TwoUniqueProds` property is a condition (not given in the provided code) typically related to the uniqueness of solutions to certain equations in the context of structures with a multiplication operation.
More concisely: If `f` is an injective group homomorphism from `H` to the group `G` with the `TwoUniqueProds` property, then `H` also has the `TwoUniqueProds` property.
|
UniqueSums.uniqueAdd_of_nonempty
theorem UniqueSums.uniqueAdd_of_nonempty :
∀ {G : Type u_1} [inst : Add G] [self : UniqueSums G] {A B : Finset G},
A.Nonempty → B.Nonempty → ∃ a0 ∈ A, ∃ b0 ∈ B, UniqueAdd A B a0 b0
The theorem `UniqueSums.uniqueAdd_of_nonempty` states that for any given type `G` equipped with an addition operation, and any two nonempty finite sets `A` and `B` of `G`, there always exist two elements `a0` in `A` and `b0` in `B` such that the sum `a0 + b0` can uniquely be written as a sum of an element from `A` and an element from `B`. In other words, if `a + b = a0 + b0` with `a` from `A` and `b` from `B`, then it must be the case that `a = a0` and `b = b0`.
More concisely: For any type `G` with addition, and nonempty finite sets `A` and `B` of `G`, there exist unique elements `a0 ∈ A` and `b0 ∈ B` such that `a0 + b0 = a + b` for all `a ∈ A` and `b ∈ B`.
|
TwoUniqueSums.uniqueAdd_of_one_lt_card
theorem TwoUniqueSums.uniqueAdd_of_one_lt_card :
∀ {G : Type u_1} [inst : Add G] [self : TwoUniqueSums G] {A B : Finset G},
1 < A.card * B.card → ∃ p1 ∈ A ×ˢ B, ∃ p2 ∈ A ×ˢ B, p1 ≠ p2 ∧ UniqueAdd A B p1.1 p1.2 ∧ UniqueAdd A B p2.1 p2.2
This theorem states that for any type `G` that supports addition and any two finite sets `A` and `B` of `G` such that the product of their cardinalities is greater than 1, there exist two distinct pairs `(p1.1, p1.2)` and `(p2.1, p2.2)` in the Cartesian product of `A` and `B` such that the sum of the elements in each pair is uniquely determined by the pair. In other words, for each pair, the sum can be expressed in exactly one way as the sum of an element from `A` and an element from `B`.
More concisely: For any type `G` with addition and finite sets `A` and `B` of `G` with cardinality product greater than 1, there exist distinct pairs `(p1, q1)` and `(p2, q2)` in `A × B` such that `p1 + q1` and `p2 + q2` are uniquely determined by the pairs.
|
UniqueAdd.addHom_map_iff
theorem UniqueAdd.addHom_map_iff :
∀ {G : Type u_1} {H : Type u_2} [inst : Add G] [inst_1 : Add H] {A B : Finset G} {a0 b0 : G} (f : G ↪ H),
(∀ (x y : G), f (x + y) = f x + f y) →
(UniqueAdd (Finset.map f A) (Finset.map f B) (f a0) (f b0) ↔ UniqueAdd A B a0 b0)
This theorem, named `UniqueAdd.addHom_map_iff`, states the following in the context of a type `G` with addition, a type `H` with addition, finite subsets `A` and `B` of `G`, and elements `a0` and `b0` of `G`:
If we have a function `f` that is an injective (embedding) and additive map from `G` to `H` (i.e., for all `x` and `y` in `G`, `f` of `x + y` equals `f` of `x` plus `f` of `y`), then the property of `UniqueAdd` (which asserts that `a0 + b0` can be written in at most one way as a sum of an element from `A` and an element from `B`) is preserved under the map `f`. This means that `UniqueAdd` holds for the image sets `Finset.map f A` and `Finset.map f B` and the elements `f a0` and `f b0` in `H` if and only if `UniqueAdd` holds for the original sets `A` and `B` and elements `a0` and `b0` in `G`.
More concisely: If `f : G → H` is an injective and additive map between additive types `G` and `H`, then `a0 + b0` has a unique representation as `x + y` with `x ∈ A` and `y ∈ B` in `G` if and only if `f(a0) + f(b0)` has a unique representation as `f(x) + f(y)` with `x ∈ Finset.map f A` and `y ∈ Finset.map f B` in `H`.
|
UniqueMul.mulHom_preimage
theorem UniqueMul.mulHom_preimage :
∀ {G : Type u_1} {H : Type u_2} [inst : Mul G] [inst_1 : Mul H] (f : G →ₙ* H) (hf : Function.Injective ⇑f)
(a0 b0 : G) {A B : Finset H}, UniqueMul A B (f a0) (f b0) → UniqueMul (A.preimage ⇑f ⋯) (B.preimage ⇑f ⋯) a0 b0
The theorem `UniqueMul.mulHom_preimage` states that the property `UniqueMul` is preserved under the inverse images of injective multiplicative maps. Specifically, if `G` and `H` are types equipped with multiplication, `f` is an injective multiplicative map from `G` to `H`, and `a0` and `b0` are elements of `G`. If `A` and `B` are finite subsets of `H` such that the product of `f a0` and `f b0` can be expressed in exactly one way as the product of an element from `A` and an element from `B`, then the corresponding property also holds for the preimages of `A` and `B` under `f` in `G` with respect to `a0` and `b0`. In other words, the product of `a0` and `b0` can be expressed in exactly one way as the product of an element from the preimage of `A` and an element from the preimage of `B`.
More concisely: If `f` is an injective multiplicative map between groups `G` and `H`, and `a0` and `b0` have unique product representations in `G` with images `fa0` and `fb0`, then `fa0` and `fb0` have unique product representations in `H` as products of elements from the preimages of finite subsets `A` and `B` under `f`, respectively.
|
TwoUniqueSums.of_injective_addHom
theorem TwoUniqueSums.of_injective_addHom :
∀ {G : Type u} {H : Type v} [inst : Add G] [inst_1 : Add H] (f : AddHom H G),
Function.Injective ⇑f → TwoUniqueSums G → TwoUniqueSums H
The theorem `TwoUniqueSums.of_injective_addHom` states that for any two types `G` and `H`, both equipped with an additive structure represented by `[Add G]` and `[Add H]` respectively, if there exists an additive homomorphism `f` from `H` to `G` that is injective (i.e., if when the function `f` maps two elements of `H` to the same element in `G`, those two elements were already the same in `H`), then the property of having "two unique sums" in `G` implies the same property in `H`. Here, "two unique sums" is a property of an additive type that ensures the uniqueness of the decomposition of every element as a sum of two others.
More concisely: If `f` is an injective additive homomorphism from an additive type `H` to an additive type `G` with the property of having two unique sums, then `H` also has the property of having two unique sums.
|
TwoUniqueProds.uniqueMul_of_one_lt_card
theorem 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
The theorem `TwoUniqueProds.uniqueMul_of_one_lt_card` asserts that for any type `G` equipped with a multiplication operation and for any two finite sets `A` and `B` of `G`, if the product of the cardinalities of `A` and `B` is greater than 1, then there exist at least two different pairs `(p1, p2)` from the Cartesian product of `A` and `B` such that both `p1` and `p2` satisfy the `UniqueMul` property. Here, `UniqueMul` property for a pair means that the product `p1.1 * p1.2` can be written in at most one way as a product of an element of `A` and an element of `B`. Similarly for `p2`.
More concisely: For any type `G` with multiplication operation and finite sets `A` and `B` of size greater than 1, there exist at least two distinct pairs `(p1, p2)` in `A × B` such that each pair satisfies the property that their product can be written as the product of an element from `A` and an element from `B` in at most one way.
|
UniqueProds.of_injective_mulHom
theorem UniqueProds.of_injective_mulHom :
∀ {G : Type u} {H : Type v} [inst : Mul G] [inst_1 : Mul H] (f : H →ₙ* G),
Function.Injective ⇑f → UniqueProds G → UniqueProds H
The theorem `UniqueProds.of_injective_mulHom` states that for any two types `G` and `H` that have multiplication (`Mul`) defined, if there is a multiplication-preserving function `f` from `H` to `G` (denoted as `f : H →ₙ* G`) that is injective (meaning that equal outputs imply equal inputs), then the property of having unique products (denoted as `UniqueProds`) is preserved from `G` to `H`. In other words, if `G` has unique products and we have an injective multiplication-preserving function from `H` to `G`, then `H` also has unique products.
More concisely: If `G` and `H` are types with multiplication, `f : H → G` is an injective multiplication-preserving function, and `G` has unique products, then `H` also has unique products.
|
UniqueProds.toTwoUniqueProds_of_group
theorem UniqueProds.toTwoUniqueProds_of_group :
∀ {G : Type u_1} [inst : Group G] [inst_1 : UniqueProds G], TwoUniqueProds G
This theorem states that if a group `G` has the property `UniqueProds`, then it also has the property `TwoUniqueProds`. In other words, in any group, if a product of elements is unique, then two such products are also unique. This is not necessarily true for semigroups that can be embedded into groups, as illustrated by Example 10.13 in J. Okniński's "Semigroup Algebras".
More concisely: If a group `G` has the property that any two distinct product expressions of elements result in equal values, then this property holds for any three product expressions.
|
UniqueMul.mulHom_image_iff
theorem UniqueMul.mulHom_image_iff :
∀ {G : Type u_1} {H : Type u_2} [inst : Mul G] [inst_1 : Mul H] {A B : Finset G} {a0 b0 : G}
[inst_2 : DecidableEq H] (f : G →ₙ* H),
Function.Injective ⇑f →
(UniqueMul (Finset.image (⇑f) A) (Finset.image (⇑f) B) (f a0) (f b0) ↔ UniqueMul A B a0 b0)
The theorem `UniqueMul.mulHom_image_iff` states that the property of `UniqueMul` is preserved under injective multiplicative maps. Given types `G` and `H` with multiplication, finite subsets `A` and `B` of `G`, and elements `a0` and `b0` of `G`, along with an injective multiplicative function `f` from `G` to `H`, the uniqueness of the product of `a0` and `b0` as a product of elements from `A` and `B` is equivalent to the uniqueness of the product of `f(a0)` and `f(b0)` as a product of elements from the images of `A` and `B` under `f`. In other words, if a unique multiplication property holds for elements in `G`, then this property also holds for their images in `H` under an injective multiplicative function.
More concisely: If `f` is an injective multiplicative function from the multiplicative monoid `(G, *)` to the multiplicative monoid `(H, *)`, then for finite sets `A` and `B` of `G`, and elements `a0` and `b0` of `G`, the uniqueness of the product `a0 * b0` from `A * B` implies the uniqueness of the product `f(a0) * f(b0)` from `f(A) * f(B)`.
|
TwoUniqueProds.mulHom_image_iff
theorem TwoUniqueProds.mulHom_image_iff :
∀ {G : Type u} {H : Type v} [inst : Mul G] [inst_1 : Mul H], G ≃* H → (TwoUniqueProds G ↔ TwoUniqueProds H) := by
sorry
This theorem, `TwoUniqueProds.mulHom_image_iff`, states that for any two types `G` and `H` that support multiplication, if there is a multiplicative equivalence between `G` and `H`, then the property of having exactly two unique products - represented by `TwoUniqueProds` - is preserved. In other words, if `G` has exactly two unique products, then `H` will also have exactly two unique products, and vice versa.
More concisely: For types `G` and `H` supporting multiplication, if there is a multiplicative equivalence between them, then `G` having exactly two unique products implies `H` also has exactly two unique products, and vice versa.
|
UniqueAdd.addHom_preimage
theorem UniqueAdd.addHom_preimage :
∀ {G : Type u_1} {H : Type u_2} [inst : Add G] [inst_1 : Add H] (f : AddHom G H) (hf : Function.Injective ⇑f)
(a0 b0 : G) {A B : Finset H}, UniqueAdd A B (f a0) (f b0) → UniqueAdd (A.preimage ⇑f ⋯) (B.preimage ⇑f ⋯) a0 b0
The theorem `UniqueAdd.addHom_preimage` states that the property of "unique addition" is preserved under the inverse images of injective additive maps. Specifically, let `G` and `H` be two types with addition, `f` be an injective additive function mapping `G` to `H`, `a0` and `b0` be two elements of `G`, and `A` and `B` be finite subsets of `H`. If the sum of `f a0` and `f b0` can be written in at most one way as the sum of an element from `A` and an element from `B` (i.e., `UniqueAdd A B (f a0) (f b0)` holds), then the same property holds for `a0` and `b0` with respect to the inverse images of `A` and `B` under `f`.
More concisely: If `f: G -> H` is an injective additive function between additive types `G` and `H`, and `A` and `B` are finite subsets of `H` such that `UniqueAdd A B (fa0) (fb0)` holds for some `a0, b0 in G`, then `UniqueAdd (f⁻¹"A") (f⁻¹"B") a0 b0` also holds.
|
UniqueSums.of_injective_addHom
theorem UniqueSums.of_injective_addHom :
∀ {G : Type u} {H : Type v} [inst : Add G] [inst_1 : Add H] (f : AddHom H G),
Function.Injective ⇑f → UniqueSums G → UniqueSums H
The theorem `UniqueSums.of_injective_addHom` states that for any two types `G` and `H` with addition structures (`Add G` and `Add H` respectively), and a function `f` from `H` to `G` that is an additive homomorphism (`AddHom H G`), if `f` is injective (i.e., different elements in `H` map to different elements in `G`), then the property of having unique sums in `G` implies the property of having unique sums in `H`. In other words, if `G` has the property that every sum of elements in `G` is unique and if there is an injective additive homomorphism from `H` to `G`, then `H` also has the property of unique sums.
More concisely: If `G` and `H` are types with addition structures, `f` is an injective additive homomorphism from `H` to `G`, and every sum of elements in `G` is unique, then every sum of elements in `H` is unique.
|
TwoUniqueSums.addHom_image_iff
theorem TwoUniqueSums.addHom_image_iff :
∀ {G : Type u} {H : Type v} [inst : Add G] [inst_1 : Add H], G ≃+ H → (TwoUniqueSums G ↔ TwoUniqueSums H) := by
sorry
This theorem states that the property `TwoUniqueSums` is preserved under additive equivalences. More specifically, for any two types `G` and `H` which have an addition operation, if `G` is additively equivalent to `H`, then `G` having the `TwoUniqueSums` property implies that `H` also has the `TwoUniqueSums` property and vice versa. The `TwoUniqueSums` property typically means that every element can be expressed as a sum of two unique elements in exactly one way.
More concisely: If types `G` and `H` with addition operations are additively equivalent, then `G` having the property that every element is the unique sum of two elements implies the same for `H`.
|
UniqueMul.mulHom_map_iff
theorem UniqueMul.mulHom_map_iff :
∀ {G : Type u_1} {H : Type u_2} [inst : Mul G] [inst_1 : Mul H] {A B : Finset G} {a0 b0 : G} (f : G ↪ H),
(∀ (x y : G), f (x * y) = f x * f y) →
(UniqueMul (Finset.map f A) (Finset.map f B) (f a0) (f b0) ↔ UniqueMul A B a0 b0)
This theorem states that for any two types `G` and `H` with multiplication, given two finite subsets `A` and `B` of `G`, and two elements `a0` and `b0` in `G`, if `f` is an injective function (an embedding) from `G` to `H` that preserves multiplication (i.e., for any pair of elements `x` and `y` in `G`, the image of their product under `f` equals the product of their images), then the property of unique multiplication (denoted by `UniqueMul`) is preserved under the mapping `f`. In other words, `a0 * b0` can be uniquely represented as a product of an element of `A` and an element of `B` if and only if the product of the images of `a0` and `b0` under `f` can be uniquely represented as a product of an element from the image of `A` under `f` and an element from the image of `B` under `f`.
More concisely: If `f` is an injective multiplication-preserving function from the multiplicatively-closed sets `A` and `B` in type `G` to type `H`, then `a0 * b0` has a unique representation as `x * y` with `x ∈ A` and `y ∈ B` if and only if `f(a0) * f(b0)` has a unique representation as `f(x) * f(y)` with `x ∈ img(A)` and `y ∈ img(B)`.
|
UniqueAdd.addHom_image_iff
theorem UniqueAdd.addHom_image_iff :
∀ {G : Type u_1} {H : Type u_2} [inst : Add G] [inst_1 : Add H] {A B : Finset G} {a0 b0 : G}
[inst_2 : DecidableEq H] (f : AddHom G H),
Function.Injective ⇑f →
(UniqueAdd (Finset.image (⇑f) A) (Finset.image (⇑f) B) (f a0) (f b0) ↔ UniqueAdd A B a0 b0)
The theorem `UniqueAdd.addHom_image_iff` states that for any two types `G` and `H` with addition, any two finite subsets `A` and `B` of `G`, and any two elements `a0` and `b0` of `G`, given an additive function `f` from `G` to `H` that is injective and `H` has decidable equality, the property of `UniqueAdd` (i.e., the property that `a0 + b0` can be expressed in at most one way as the sum of an element from `A` and an element from `B`) is preserved under the function `f`. That is, `UniqueAdd` holds for the images of `A` and `B` under `f` and the images of `a0` and `b0` under `f` if and only if `UniqueAdd` holds for `A`, `B`, `a0`, and `b0`.
More concisely: If `f : G -> H` is an injective add function between additive types `G` and `H` with decidable equality, then the property of `A` and `B` subsets of `G` having at most one element sum representing a given element `c` (denoted as `UniqueAdd(A, B, c)`) is preserved under the image `f`, i.e., `UniqueAdd(f(A), f(B), f(c))` holds if and only if `UniqueAdd(A, B, c)` holds.
|
UniqueMul.of_mulOpposite
theorem UniqueMul.of_mulOpposite :
∀ {G : Type u_1} [inst : Mul G] {A B : Finset G} {a0 b0 : G},
UniqueMul (Finset.map { toFun := MulOpposite.op, inj' := ⋯ } B)
(Finset.map { toFun := MulOpposite.op, inj' := ⋯ } A) (MulOpposite.op b0) (MulOpposite.op a0) →
UniqueMul A B a0 b0
The theorem `UniqueMul.of_mulOpposite` states the following:
For any type `G` equipped with a multiplication operation, two finite subsets `A` and `B` of `G`, and two elements `a0` and `b0` of `G`, if the product `MulOpposite.op b0 * MulOpposite.op a0` can be written in at most one way as a product of an element from the image set of `B` under the operation `MulOpposite.op` and an element from the image set of `A` under the same operation, then the product `a0 * b0` can be written in at most one way as a product of an element from `A` and an element from `B`. In other words, uniqueness of multiplication in the opposite multiplicative structure implies uniqueness of multiplication in the original structure.
More concisely: If the product of the opposites of two elements has at most one representation as a product of elements from two sets under multiplication, then the product of the original elements has at most one representation as a product of an element from each set.
|