Unique products and related notions

A group G has unique products if for any two non-empty finite subsets A, B ⊆ G, there is an element g ∈ A * B that can be written uniquely as a product of an element of A and an element of B. We call the formalization this property UniqueProds. Since the condition requires no property of the group operation, we define it for a Type simply satisfying Mul. We also introduce the analogous "additive" companion, UniqueSums, and link the two so that to_additive converts UniqueProds into UniqueSums.

A common way of proving that a group satisfies the UniqueProds/Sums property is by assuming the existence of some kind of ordering on the group that is well-behaved with respect to the group operation and showing that minima/maxima are the "unique products/sums". However, the order is just a convenience and is not part of the UniqueProds/Sums setup.

Here you can see several examples of Types that have UniqueSums/Prods (inferInstance uses Covariant.to_uniqueProds_left and Covariant.to_uniqueSums_left).

import Mathlib.Data.Real.Basic
import Mathlib.Data.PNat.Basic
import Mathlib.Algebra.Group.UniqueProds

example : UniqueSums ℕ   := inferInstance
example : UniqueSums ℕ+  := inferInstance
example : UniqueSums ℤ   := inferInstance
example : UniqueSums ℚ   := inferInstance
example : UniqueSums ℝ   := inferInstance
example : UniqueProds ℕ+ := inferInstance

Use in (Add)MonoidAlgebras

UniqueProds/Sums allow to decouple certain arguments about (Add)MonoidAlgebras into an argument about the grading type and then a generic statement of the form "look at the coefficient of the 'unique product/sum'". The file Algebra/MonoidAlgebra/NoZeroDivisors contains several examples of this use.

def UniqueAdd {G : Type u_1} [Add G] (A : Finset G) (B : Finset G) (a0 : G) (b0 : G) : Prop

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 : Type u_1} [Mul G] (A : Finset G) (B : Finset G) (a0 : G) (b0 : G) : Prop

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.

@[simp]

theorem UniqueAdd.of_subsingleton {G : Type u_1} [Add G] {A : Finset G} {B : Finset G} {a0 : G} {b0 : G} [Subsingleton G] : UniqueAdd A B a0 b0

@[simp]

theorem UniqueMul.of_subsingleton {G : Type u_1} [Mul G] {A : Finset G} {B : Finset G} {a0 : G} {b0 : G} [Subsingleton G] : UniqueMul A B a0 b0

theorem UniqueAdd.of_card_nonpos {G : Type u_1} [Add G] {A : Finset G} {B : Finset G} (hA : Finset.Nonempty A) (hB : Finset.Nonempty B) (hA1 : Finset.card A ≤ 1) (hB1 : Finset.card B ≤ 1) : ∃ a, a ∈ A ∧ ∃ b, b ∈ B ∧ UniqueAdd A B a b

theorem UniqueMul.of_card_le_one {G : Type u_1} [Mul G] {A : Finset G} {B : Finset G} (hA : Finset.Nonempty A) (hB : Finset.Nonempty B) (hA1 : Finset.card A ≤ 1) (hB1 : Finset.card B ≤ 1) : ∃ a, a ∈ A ∧ ∃ b, b ∈ B ∧ UniqueMul A B a b

theorem UniqueAdd.mt {G : Type u_1} [Add G] {A : Finset G} {B : Finset G} {a0 : G} {b0 : G} (h : UniqueAdd A B a0 b0) ⦃a : G⦄ ⦃b : G⦄ : a ∈ A → b ∈ B → a ≠ a0 ∨ b ≠ b0 → a + b ≠ a0 + b0

theorem UniqueMul.mt {G : Type u_1} [Mul G] {A : Finset G} {B : Finset G} {a0 : G} {b0 : G} (h : UniqueMul A B a0 b0) ⦃a : G⦄ ⦃b : G⦄ : a ∈ A → b ∈ B → a ≠ a0 ∨ b ≠ b0 → a * b ≠ a0 * b0

theorem UniqueAdd.subsingleton {G : Type u_1} [Add G] {A : Finset G} {B : Finset G} {a0 : G} {b0 : G} (h : UniqueAdd A B a0 b0) : Subsingleton { ab // ab.fst ∈ A ∧ ab.snd ∈ B ∧ ab.fst + ab.snd = a0 + b0 }

abbrev UniqueAdd.subsingleton.match_1 {G : Type u_1} [Add G] {A : Finset G} {B : Finset G} {a0 : G} {b0 : G} (motive : { ab // ab.fst ∈ A ∧ ab.snd ∈ B ∧ ab.fst + ab.snd = a0 + b0 } → Prop) : (x : { ab // ab.fst ∈ A ∧ ab.snd ∈ B ∧ ab.fst + ab.snd = a0 + b0 }) → ((_a' _b' : G) → (ha' : (_a', _b').fst ∈ A) → (hb' : (_a', _b').snd ∈ B) → (ab' : (_a', _b').fst + (_a', _b').snd = a0 + b0) → motive { val := (_a', _b'), property := (_ : (_a', _b').fst ∈ A ∧ (_a', _b').snd ∈ B ∧ (_a', _b').fst + (_a', _b').snd = a0 + b0) }) → motive x

theorem UniqueMul.subsingleton {G : Type u_1} [Mul G] {A : Finset G} {B : Finset G} {a0 : G} {b0 : G} (h : UniqueMul A B a0 b0) : Subsingleton { ab // ab.fst ∈ A ∧ ab.snd ∈ B ∧ ab.fst * ab.snd = a0 * b0 }

theorem UniqueAdd.set_subsingleton {G : Type u_1} [Add G] {A : Finset G} {B : Finset G} {a0 : G} {b0 : G} (h : UniqueAdd A B a0 b0) : Set.Subsingleton {ab | ab.fst ∈ A ∧ ab.snd ∈ B ∧ ab.fst + ab.snd = a0 + b0}

theorem UniqueMul.set_subsingleton {G : Type u_1} [Mul G] {A : Finset G} {B : Finset G} {a0 : G} {b0 : G} (h : UniqueMul A B a0 b0) : Set.Subsingleton {ab | ab.fst ∈ A ∧ ab.snd ∈ B ∧ ab.fst * ab.snd = a0 * b0}

theorem UniqueAdd.iff_existsUnique {G : Type u_1} [Add G] {A : Finset G} {B : Finset G} {a0 : G} {b0 : G} (aA : a0 ∈ A) (bB : b0 ∈ B) : UniqueAdd A B a0 b0 ↔ ∃! ab, ab ∈ A ×ˢ B ∧ ab.fst + ab.snd = a0 + b0

theorem UniqueMul.iff_existsUnique {G : Type u_1} [Mul G] {A : Finset G} {B : Finset G} {a0 : G} {b0 : G} (aA : a0 ∈ A) (bB : b0 ∈ B) : UniqueMul A B a0 b0 ↔ ∃! ab, ab ∈ A ×ˢ B ∧ ab.fst * ab.snd = a0 * b0

abbrev UniqueAdd.iff_card_nonpos.match_1 {G : Type u_1} [Add G] {A : Finset G} {B : Finset G} {a0 : G} {b0 : G} (p2 : G × G) (motive : (p2.fst ∈ A ∧ p2.snd ∈ B) ∧ p2.fst + p2.snd = a0 + b0 → Prop) : (x : (p2.fst ∈ A ∧ p2.snd ∈ B) ∧ p2.fst + p2.snd = a0 + b0) → ((ha2 : p2.fst ∈ A) → (hb2 : p2.snd ∈ B) → (he2 : p2.fst + p2.snd = a0 + b0) → motive (_ : (p2.fst ∈ A ∧ p2.snd ∈ B) ∧ p2.fst + p2.snd = a0 + b0)) → motive x

theorem UniqueAdd.iff_card_nonpos {G : Type u_1} [Add G] {A : Finset G} {B : Finset G} {a0 : G} {b0 : G} [DecidableEq G] (ha0 : a0 ∈ A) (hb0 : b0 ∈ B) : UniqueAdd A B a0 b0 ↔ Finset.card (Finset.filter (fun p => p.fst + p.snd = a0 + b0) (A ×ˢ B)) ≤ 1

theorem UniqueMul.iff_card_le_one {G : Type u_1} [Mul G] {A : Finset G} {B : Finset G} {a0 : G} {b0 : G} [DecidableEq G] (ha0 : a0 ∈ A) (hb0 : b0 ∈ B) : UniqueMul A B a0 b0 ↔ Finset.card (Finset.filter (fun p => p.fst * p.snd = a0 * b0) (A ×ˢ B)) ≤ 1

abbrev UniqueAdd.exists_iff_exists_existsUnique.match_2 {G : Type u_1} [Add G] {A : Finset G} {B : Finset G} (motive : (∃ g, ∃! ab, ab ∈ A ×ˢ B ∧ ab.fst + ab.snd = g) → Prop) : (x : ∃ g, ∃! ab, ab ∈ A ×ˢ B ∧ ab.fst + ab.snd = g) → ((g : G) → (h : ∃! ab, ab ∈ A ×ˢ B ∧ ab.fst + ab.snd = g) → motive (_ : ∃ g, ∃! ab, ab ∈ A ×ˢ B ∧ ab.fst + ab.snd = g)) → motive x

theorem UniqueAdd.exists_iff_exists_existsUnique {G : Type u_1} [Add G] {A : Finset G} {B : Finset G} : (∃ a0 b0, a0 ∈ A ∧ b0 ∈ B ∧ UniqueAdd A B a0 b0) ↔ ∃ g, ∃! ab, ab ∈ A ×ˢ B ∧ ab.fst + ab.snd = g

abbrev UniqueAdd.exists_iff_exists_existsUnique.match_1 {G : Type u_1} [Add G] {A : Finset G} {B : Finset G} (motive : (∃ a0 b0, a0 ∈ A ∧ b0 ∈ B ∧ UniqueAdd A B a0 b0) → Prop) : (x : ∃ a0 b0, a0 ∈ A ∧ b0 ∈ B ∧ UniqueAdd A B a0 b0) → ((a0 b0 : G) → (hA : a0 ∈ A) → (hB : b0 ∈ B) → (h : UniqueAdd A B a0 b0) → motive (_ : ∃ a0 b0, a0 ∈ A ∧ b0 ∈ B ∧ UniqueAdd A B a0 b0)) → motive x

theorem UniqueMul.exists_iff_exists_existsUnique {G : Type u_1} [Mul G] {A : Finset G} {B : Finset G} : (∃ a0 b0, a0 ∈ A ∧ b0 ∈ B ∧ UniqueMul A B a0 b0) ↔ ∃ g, ∃! ab, ab ∈ A ×ˢ B ∧ ab.fst * ab.snd = g

theorem UniqueAdd.addHom_preimage {G : Type u_1} {H : Type u_2} [Add G] [Add H] (f : AddHom G H) (hf : Function.Injective ↑f) (a0 : G) (b0 : G) {A : Finset H} {B : Finset H} (u : UniqueAdd A B (↑f a0) (↑f b0)) : UniqueAdd (Finset.preimage A ↑f (_ : Set.InjOn (↑f) (↑f ⁻¹' ↑A))) (Finset.preimage B ↑f (_ : Set.InjOn (↑f) (↑f ⁻¹' ↑B))) a0 b0

UniqueAdd is preserved by inverse images under injective, additive maps.

theorem UniqueMul.mulHom_preimage {G : Type u_1} {H : Type u_2} [Mul G] [Mul H] (f : G →ₙ* H) (hf : Function.Injective ↑f) (a0 : G) (b0 : G) {A : Finset H} {B : Finset H} (u : UniqueMul A B (↑f a0) (↑f b0)) : UniqueMul (Finset.preimage A ↑f (_ : Set.InjOn (↑f) (↑f ⁻¹' ↑A))) (Finset.preimage B ↑f (_ : Set.InjOn (↑f) (↑f ⁻¹' ↑B))) a0 b0

UniqueMul is preserved by inverse images under injective, multiplicative maps.

theorem UniqueAdd.addHom_image_iff {G : Type u_1} {H : Type u_2} [Add G] [Add H] {A : Finset G} {B : Finset G} {a0 : G} {b0 : G} [DecidableEq H] (f : AddHom G H) (hf : Function.Injective ↑f) : UniqueAdd (Finset.image (↑f) A) (Finset.image (↑f) B) (↑f a0) (↑f b0) ↔ UniqueAdd A B a0 b0

UniqueAdd is preserved under additive maps that are injective.

See UniqueAdd.addHom_map_iff for a version with swapped bundling.

theorem UniqueMul.mulHom_image_iff {G : Type u_1} {H : Type u_2} [Mul G] [Mul H] {A : Finset G} {B : Finset G} {a0 : G} {b0 : G} [DecidableEq H] (f : G →ₙ* H) (hf : Function.Injective ↑f) : UniqueMul (Finset.image (↑f) A) (Finset.image (↑f) B) (↑f a0) (↑f b0) ↔ UniqueMul A B a0 b0

Unique_Mul is preserved under multiplicative maps that are injective.

See UniqueMul.mulHom_map_iff for a version with swapped bundling.

theorem UniqueAdd.addHom_map_iff {G : Type u_1} {H : Type u_2} [Add G] [Add H] {A : Finset G} {B : Finset G} {a0 : G} {b0 : G} (f : G ↪ H) (mul : ∀ (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

UniqueAdd is preserved under embeddings that are additive.

See UniqueAdd.addHom_image_iff for a version with swapped bundling.

theorem UniqueMul.mulHom_map_iff {G : Type u_1} {H : Type u_2} [Mul G] [Mul H] {A : Finset G} {B : Finset G} {a0 : G} {b0 : G} (f : G ↪ H) (mul : ∀ (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

UniqueMul is preserved under embeddings that are multiplicative.

See UniqueMul.mulHom_image_iff for a version with swapped bundling.

theorem UniqueAdd.of_addOpposite {G : Type u_1} [Add G] {A : Finset G} {B : Finset G} {a0 : G} {b0 : G} (h : UniqueAdd (Finset.map { toFun := AddOpposite.op, inj' := (_ : Function.Injective AddOpposite.op) } B) (Finset.map { toFun := AddOpposite.op, inj' := (_ : Function.Injective AddOpposite.op) } A) (AddOpposite.op b0) (AddOpposite.op a0)) : UniqueAdd A B a0 b0

theorem UniqueMul.of_mulOpposite {G : Type u_1} [Mul G] {A : Finset G} {B : Finset G} {a0 : G} {b0 : G} (h : UniqueMul (Finset.map { toFun := MulOpposite.op, inj' := (_ : Function.Injective MulOpposite.op) } B) (Finset.map { toFun := MulOpposite.op, inj' := (_ : Function.Injective MulOpposite.op) } A) (MulOpposite.op b0) (MulOpposite.op a0)) : UniqueMul A B a0 b0

theorem UniqueAdd.to_addOpposite {G : Type u_1} [Add G] {A : Finset G} {B : Finset G} {a0 : G} {b0 : G} (h : UniqueAdd A B a0 b0) : UniqueAdd (Finset.map { toFun := AddOpposite.op, inj' := (_ : Function.Injective AddOpposite.op) } B) (Finset.map { toFun := AddOpposite.op, inj' := (_ : Function.Injective AddOpposite.op) } A) (AddOpposite.op b0) (AddOpposite.op a0)

theorem UniqueMul.to_mulOpposite {G : Type u_1} [Mul G] {A : Finset G} {B : Finset G} {a0 : G} {b0 : G} (h : UniqueMul A B a0 b0) : UniqueMul (Finset.map { toFun := MulOpposite.op, inj' := (_ : Function.Injective MulOpposite.op) } B) (Finset.map { toFun := MulOpposite.op, inj' := (_ : Function.Injective MulOpposite.op) } A) (MulOpposite.op b0) (MulOpposite.op a0)

theorem UniqueAdd.iff_addOpposite {G : Type u_1} [Add G] {A : Finset G} {B : Finset G} {a0 : G} {b0 : G} : UniqueAdd (Finset.map { toFun := AddOpposite.op, inj' := (_ : Function.Injective AddOpposite.op) } B) (Finset.map { toFun := AddOpposite.op, inj' := (_ : Function.Injective AddOpposite.op) } A) (AddOpposite.op b0) (AddOpposite.op a0) ↔ UniqueAdd A B a0 b0

theorem UniqueMul.iff_mulOpposite {G : Type u_1} [Mul G] {A : Finset G} {B : Finset G} {a0 : G} {b0 : G} : UniqueMul (Finset.map { toFun := MulOpposite.op, inj' := (_ : Function.Injective MulOpposite.op) } B) (Finset.map { toFun := MulOpposite.op, inj' := (_ : Function.Injective MulOpposite.op) } A) (MulOpposite.op b0) (MulOpposite.op a0) ↔ UniqueMul A B a0 b0

theorem UniqueAdd.of_image_filter {G : Type u_1} {H : Type u_2} [Add G] [Add H] [DecidableEq H] (f : AddHom G H) {A : Finset G} {B : Finset G} {aG : G} {bG : G} {aH : H} {bH : H} (hae : ↑f aG = aH) (hbe : ↑f bG = bH) (huH : UniqueAdd (Finset.image (↑f) A) (Finset.image (↑f) B) aH bH) (huG : UniqueAdd (Finset.filter (fun x => ↑f x = aH) A) (Finset.filter (fun x => ↑f x = bH) B) aG bG) : UniqueAdd A B aG bG

theorem UniqueMul.of_image_filter {G : Type u_1} {H : Type u_2} [Mul G] [Mul H] [DecidableEq H] (f : G →ₙ* H) {A : Finset G} {B : Finset G} {aG : G} {bG : G} {aH : H} {bH : H} (hae : ↑f aG = aH) (hbe : ↑f bG = bH) (huH : UniqueMul (Finset.image (↑f) A) (Finset.image (↑f) B) aH bH) (huG : UniqueMul (Finset.filter (fun x => ↑f x = aH) A) (Finset.filter (fun x => ↑f x = bH) B) aG bG) : UniqueMul A B aG bG

class UniqueSums (G : Type u_1) [Add G] : Prop

• uniqueAdd_of_nonempty : ∀ {A B : Finset G}, Finset.Nonempty A → Finset.Nonempty B → ∃ a0, a0 ∈ A ∧ ∃ b0, b0 ∈ B ∧ UniqueAdd A B a0 b0

  For A B two nonempty finite sets, there always exist a0 ∈ A, b0 ∈ B such that UniqueAdd A B a0 b0

Let G be a Type with addition. UniqueSums G asserts that any two non-empty finite subsets of G have the UniqueAdd property, with respect to some element of their sum A + B.

class UniqueProds (G : Type u_1) [Mul G] : Prop

• uniqueMul_of_nonempty : ∀ {A B : Finset G}, Finset.Nonempty A → Finset.Nonempty B → ∃ a0, a0 ∈ A ∧ ∃ b0, b0 ∈ B ∧ UniqueMul A B a0 b0

  For A B two nonempty finite sets, there always exist a0 ∈ A, b0 ∈ B such that UniqueMul A B a0 b0

Let G be a Type with multiplication. UniqueProds G asserts that any two non-empty finite subsets of G have the UniqueMul property, with respect to some element of their product A * B.

class TwoUniqueSums (G : Type u_1) [Add G] : Prop

• uniqueAdd_of_one_lt_card : ∀ {A B : Finset G}, 1 < Finset.card A * Finset.card B → ∃ p1, p1 ∈ A ×ˢ B ∧ ∃ p2, p2 ∈ A ×ˢ B ∧ p1 ≠ p2 ∧ UniqueAdd A B p1.fst p1.snd ∧ UniqueAdd A B p2.fst p2.snd

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

Let G be a Type with addition. TwoUniqueSums G asserts that any two non-empty finite subsets of G, at least one of which is not a singleton, possesses at least two pairs of elements satisfying the UniqueAdd property.

class TwoUniqueProds (G : Type u_1) [Mul G] : Prop

• uniqueMul_of_one_lt_card : ∀ {A B : Finset G}, 1 < Finset.card A * Finset.card B → ∃ p1, p1 ∈ A ×ˢ B ∧ ∃ p2, p2 ∈ A ×ˢ B ∧ p1 ≠ p2 ∧ UniqueMul A B p1.fst p1.snd ∧ UniqueMul A B p2.fst p2.snd

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

Let G be a Type with multiplication. TwoUniqueProds G asserts that any two non-empty finite subsets of G, at least one of which is not a singleton, possesses at least two pairs of elements satisfying the UniqueMul property.

theorem uniqueAdd_of_twoUniqueAdd {G : Type u_1} [Add G] {A : Finset G} {B : Finset G} (h : 1 < Finset.card A * Finset.card B → ∃ p1, p1 ∈ A ×ˢ B ∧ ∃ p2, p2 ∈ A ×ˢ B ∧ p1 ≠ p2 ∧ UniqueAdd A B p1.fst p1.snd ∧ UniqueAdd A B p2.fst p2.snd) (hA : Finset.Nonempty A) (hB : Finset.Nonempty B) : ∃ a, a ∈ A ∧ ∃ b, b ∈ B ∧ UniqueAdd A B a b

theorem uniqueMul_of_twoUniqueMul {G : Type u_1} [Mul G] {A : Finset G} {B : Finset G} (h : 1 < Finset.card A * Finset.card B → ∃ p1, p1 ∈ A ×ˢ B ∧ ∃ p2, p2 ∈ A ×ˢ B ∧ p1 ≠ p2 ∧ UniqueMul A B p1.fst p1.snd ∧ UniqueMul A B p2.fst p2.snd) (hA : Finset.Nonempty A) (hB : Finset.Nonempty B) : ∃ a, a ∈ A ∧ ∃ b, b ∈ B ∧ UniqueMul A B a b

theorem TwoUniqueSums.toUniqueSums.proof_1 (G : Type u_1) [Add G] [TwoUniqueSums G] : UniqueSums G

instance TwoUniqueSums.toUniqueSums (G : Type u_1) [Add G] [TwoUniqueSums G] : UniqueSums G

instance TwoUniqueProds.toUniqueProds (G : Type u_1) [Mul G] [TwoUniqueProds G] : UniqueProds G

instance Multiplicative.instUniqueProdsMultiplicativeMul {M : Type u_1} [Add M] [UniqueSums M] : UniqueProds (Multiplicative M)

instance Multiplicative.instTwoUniqueProdsMultiplicativeMul {M : Type u_1} [Add M] [TwoUniqueSums M] : TwoUniqueProds (Multiplicative M)

instance Additive.instUniqueSumsAdditiveAdd {M : Type u_1} [Mul M] [UniqueProds M] : UniqueSums (Additive M)

instance Additive.instTwoUniqueSumsAdditiveAdd {M : Type u_1} [Mul M] [TwoUniqueProds M] : TwoUniqueSums (Additive M)

theorem UniqueSums.addHom_image_of_injective {G : Type u} {H : Type v} [Add G] [Add H] (f : AddHom H G) (hf : Function.Injective ↑f) (uG : UniqueSums G) : UniqueSums H

theorem UniqueProds.mulHom_image_of_injective {G : Type u} {H : Type v} [Mul G] [Mul H] (f : H →ₙ* G) (hf : Function.Injective ↑f) (uG : UniqueProds G) : UniqueProds H

theorem UniqueSums.addHom_image_iff {G : Type u} {H : Type v} [Add G] [Add H] (f : G ≃+ H) : UniqueSums G ↔ UniqueSums H

UniqueSums is preserved under additive equivalences.

theorem UniqueProds.mulHom_image_iff {G : Type u} {H : Type v} [Mul G] [Mul H] (f : G ≃* H) : UniqueProds G ↔ UniqueProds H

UniqueProd is preserved under multiplicative equivalences.

abbrev UniqueSums.of_addOpposite.match_1 {G : Type u_1} [Add G] : ∀ {A B : Finset G} (f : G ↪ Gᵃᵒᵖ) (motive : (∃ a0, a0 ∈ Finset.map f B ∧ ∃ b0, b0 ∈ Finset.map f A ∧ UniqueAdd (Finset.map f B) (Finset.map f A) a0 b0) → Prop) (x : ∃ a0, a0 ∈ Finset.map f B ∧ ∃ b0, b0 ∈ Finset.map f A ∧ UniqueAdd (Finset.map f B) (Finset.map f A) a0 b0), (∀ (y : Gᵃᵒᵖ) (yB : y ∈ Finset.map f B) (x : Gᵃᵒᵖ) (xA : x ∈ Finset.map f A) (hxy : UniqueAdd (Finset.map f B) (Finset.map f A) y x), motive (_ : ∃ a0, a0 ∈ Finset.map f B ∧ ∃ b0, b0 ∈ Finset.map f A ∧ UniqueAdd (Finset.map f B) (Finset.map f A) a0 b0)) → motive x

theorem UniqueSums.of_addOpposite {G : Type u} [Add G] (h : UniqueSums Gᵃᵒᵖ) : UniqueSums G

theorem UniqueProds.of_mulOpposite {G : Type u} [Mul G] (h : UniqueProds Gᵐᵒᵖ) : UniqueProds G

instance UniqueSums.instUniqueSumsAddOppositeAdd {G : Type u} [Add G] [h : UniqueSums G] : UniqueSums Gᵃᵒᵖ

theorem UniqueSums.instUniqueSumsAddOppositeAdd.proof_1 {G : Type u_1} [Add G] [h : UniqueSums G] : UniqueSums Gᵃᵒᵖ

instance UniqueProds.instUniqueProdsMulOppositeMul {G : Type u} [Mul G] [h : UniqueProds G] : UniqueProds Gᵐᵒᵖ

theorem UniqueSums.toIsAddCancel {G : Type u} [Add G] [UniqueSums G] : IsCancelAdd G

theorem UniqueProds.toIsCancelMul {G : Type u} [Mul G] [UniqueProds G] : IsCancelMul G

Two theorems in [Andrzej Strojnowski, A note on u.p. groups][Strojnowski1980]

theorem UniqueSums.of_same {G : Type u_1} [AddSemigroup G] [IsCancelAdd G] (h : ∀ {A : Finset G}, Finset.Nonempty A → ∃ a1, a1 ∈ A ∧ ∃ a2, a2 ∈ A ∧ UniqueAdd A A a1 a2) : UniqueSums G

theorem UniqueProds.of_same {G : Type u_1} [Semigroup G] [IsCancelMul G] (h : ∀ {A : Finset G}, Finset.Nonempty A → ∃ a1, a1 ∈ A ∧ ∃ a2, 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.

theorem UniqueSums.toTwoUniqueSums_of_addGroup {G : Type u_1} [AddGroup G] [UniqueSums G] : TwoUniqueSums G

theorem UniqueProds.toTwoUniqueProds_of_group {G : Type u_1} [Group G] [UniqueProds G] : TwoUniqueProds G

If a group has UniqueProds, then it actually has TwoUniqueProds. For an example of a semigroup G embeddable into a group that has UniqueProds but not TwoUniqueProds, see Example 10.13 in [J. Okniński, Semigroup Algebras][Okninski1991].

theorem UniqueSums.instUniqueSumsForAllInstAdd.proof_1 {ι : Type u_1} (G : ι → Type u_2) [(i : ι) → Add (G i)] [∀ (i : ι), UniqueSums (G i)] : UniqueSums ((i : ι) → G i)

instance UniqueSums.instUniqueSumsForAllInstAdd {ι : Type u_2} (G : ι → Type u_1) [(i : ι) → Add (G i)] [∀ (i : ι), UniqueSums (G i)] : UniqueSums ((i : ι) → G i)

instance UniqueProds.instUniqueProdsForAllInstMul {ι : Type u_2} (G : ι → Type u_1) [(i : ι) → Mul (G i)] [∀ (i : ι), UniqueProds (G i)] : UniqueProds ((i : ι) → G i)

theorem UniqueSums.instUniqueSumsSumInstAdd.proof_1 {G : Type u_1} {H : Type u_2} [Add G] [Add H] [UniqueSums G] [UniqueSums H] : UniqueSums (G × H)

instance UniqueSums.instUniqueSumsSumInstAdd {G : Type u} {H : Type v} [Add G] [Add H] [UniqueSums G] [UniqueSums H] : UniqueSums (G × H)

instance UniqueProds.instUniqueProdsProdInstMul {G : Type u} {H : Type v} [Mul G] [Mul H] [UniqueProds G] [UniqueProds H] : UniqueProds (G × H)

instance instUniqueSumsDFinsuppToZeroInstAddDFinsuppToZero {ι : Type u_2} (G : ι → Type u_1) [(i : ι) → AddZeroClass (G i)] [∀ (i : ι), UniqueSums (G i)] : UniqueSums (Π₀ (i : ι), G i)

instance instUniqueSumsFinsuppToZeroAdd {ι : Type u_1} {G : Type u_2} [AddZeroClass G] [UniqueSums G] : UniqueSums (ι →₀ G)

theorem TwoUniqueSums.addHom_image_of_injective {G : Type u} {H : Type v} [Add G] [Add H] (f : AddHom H G) (hf : Function.Injective ↑f) (uG : TwoUniqueSums G) : TwoUniqueSums H

theorem TwoUniqueProds.mulHom_image_of_injective {G : Type u} {H : Type v} [Mul G] [Mul H] (f : H →ₙ* G) (hf : Function.Injective ↑f) (uG : TwoUniqueProds G) : TwoUniqueProds H

theorem TwoUniqueSums.addHom_image_iff {G : Type u} {H : Type v} [Add G] [Add H] (f : G ≃+ H) : TwoUniqueSums G ↔ TwoUniqueSums H

TwoUniqueSums is preserved under additive equivalences.

theorem TwoUniqueProds.mulHom_image_iff {G : Type u} {H : Type v} [Mul G] [Mul H] (f : G ≃* H) : TwoUniqueProds G ↔ TwoUniqueProds H

TwoUniqueProd is preserved under multiplicative equivalences.

instance TwoUniqueSums.instTwoUniqueSumsForAllInstAdd {ι : Type u_2} (G : ι → Type u_1) [(i : ι) → Add (G i)] [∀ (i : ι), TwoUniqueSums (G i)] : TwoUniqueSums ((i : ι) → G i)

theorem TwoUniqueSums.instTwoUniqueSumsForAllInstAdd.proof_1 {ι : Type u_1} (G : ι → Type u_2) [(i : ι) → Add (G i)] [∀ (i : ι), TwoUniqueSums (G i)] : TwoUniqueSums ((i : ι) → G i)

instance TwoUniqueProds.instTwoUniqueProdsForAllInstMul {ι : Type u_2} (G : ι → Type u_1) [(i : ι) → Mul (G i)] [∀ (i : ι), TwoUniqueProds (G i)] : TwoUniqueProds ((i : ι) → G i)

theorem TwoUniqueSums.instTwoUniqueSumsSumInstAdd.proof_1 {G : Type u_1} {H : Type u_2} [Add G] [Add H] [TwoUniqueSums G] [TwoUniqueSums H] : TwoUniqueSums (G × H)

instance TwoUniqueSums.instTwoUniqueSumsSumInstAdd {G : Type u} {H : Type v} [Add G] [Add H] [TwoUniqueSums G] [TwoUniqueSums H] : TwoUniqueSums (G × H)

instance TwoUniqueProds.instTwoUniqueProdsProdInstMul {G : Type u} {H : Type v} [Mul G] [Mul H] [TwoUniqueProds G] [TwoUniqueProds H] : TwoUniqueProds (G × H)

theorem TwoUniqueSums.of_addOpposite {G : Type u} [Add G] (h : TwoUniqueSums Gᵃᵒᵖ) : TwoUniqueSums G

theorem TwoUniqueProds.of_mulOpposite {G : Type u} [Mul G] (h : TwoUniqueProds Gᵐᵒᵖ) : TwoUniqueProds G

instance TwoUniqueSums.instTwoUniqueSumsAddOppositeAdd {G : Type u} [Add G] [h : TwoUniqueSums G] : TwoUniqueSums Gᵃᵒᵖ

theorem TwoUniqueSums.instTwoUniqueSumsAddOppositeAdd.proof_1 {G : Type u_1} [Add G] [h : TwoUniqueSums G] : TwoUniqueSums Gᵃᵒᵖ

instance TwoUniqueProds.instTwoUniqueProdsMulOppositeMul {G : Type u} [Mul G] [h : TwoUniqueProds G] : TwoUniqueProds Gᵐᵒᵖ

theorem TwoUniqueSums.of_Covariant_right.proof_1 {G : Type u_1} [Add G] [IsRightCancelAdd G] [LinearOrder G] [CovariantClass G G (fun x x_1 => x + x_1) fun x x_1 => x < x_1] : TwoUniqueSums G

instance TwoUniqueSums.of_Covariant_right {G : Type u} [Add G] [IsRightCancelAdd G] [LinearOrder G] [CovariantClass G G (fun x x_1 => x + x_1) fun x x_1 => x < x_1] : TwoUniqueSums G

This instance asserts that if G has a right-cancellative addition, a linear order, and addition is strictly monotone w.r.t. the second argument, then G has TwoUniqueSums.

instance TwoUniqueProds.of_Covariant_right {G : Type u} [Mul G] [IsRightCancelMul G] [LinearOrder G] [CovariantClass G G (fun x x_1 => x * x_1) fun x x_1 => x < x_1] : TwoUniqueProds G

This instance asserts that if G has a right-cancellative multiplication, a linear order, and multiplication is strictly monotone w.r.t. the second argument, then G has TwoUniqueProds.

theorem TwoUniqueSums.of_Covariant_left.proof_1 {G : Type u_1} [Add G] [IsLeftCancelAdd G] [LinearOrder G] [CovariantClass G G (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1] : TwoUniqueSums G

instance TwoUniqueSums.of_Covariant_left {G : Type u} [Add G] [IsLeftCancelAdd G] [LinearOrder G] [CovariantClass G G (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1] : TwoUniqueSums G

This instance asserts that if G has a left-cancellative addition, a linear order, and addition is strictly monotone w.r.t. the first argument, then G has TwoUniqueSums.

instance TwoUniqueProds.of_Covariant_left {G : Type u} [Mul G] [IsLeftCancelMul G] [LinearOrder G] [CovariantClass G G (Function.swap fun x x_1 => x * x_1) fun x x_1 => x < x_1] : TwoUniqueProds G

This instance asserts that if G has a left-cancellative multiplication, a linear order, and multiplication is strictly monotone w.r.t. the first argument, then G has TwoUniqueProds.

instance instTwoUniqueSumsDFinsuppToZeroInstAddDFinsuppToZero {ι : Type u_2} (G : ι → Type u_1) [(i : ι) → AddZeroClass (G i)] [∀ (i : ι), TwoUniqueSums (G i)] : TwoUniqueSums (Π₀ (i : ι), G i)

instance instTwoUniqueSumsFinsuppToZeroAdd {ι : Type u_1} {G : Type u_2} [AddZeroClass G] [TwoUniqueSums G] : TwoUniqueSums (ι →₀ G)

instance instTwoUniqueSumsToAddToAddSemigroupToAddMonoidToSubNegMonoidToAddGroup {G : Type u} [AddCommGroup G] [Module ℚ G] : TwoUniqueSums G

Any ℚ-vector space has TwoUniqueSums, because it is isomorphic to some (Basis.ofVectorSpaceIndex ℚ G) →₀ ℚ by choosing a basis, and ℚ already has TwoUniqueSums because it's ordered.