# 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 : ) (B : ) (a0 : G) (b0 : G) :

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.

Equations
Instances For
def UniqueMul {G : Type u_1} [Mul G] (A : ) (B : ) (a0 : G) (b0 : G) :

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.

Equations
Instances For
@[simp]
theorem UniqueAdd.of_subsingleton {G : Type u_1} [Add G] {A : } {B : } {a0 : G} {b0 : G} [] :
UniqueAdd A B a0 b0
@[simp]
theorem UniqueMul.of_subsingleton {G : Type u_1} [Mul G] {A : } {B : } {a0 : G} {b0 : G} [] :
UniqueMul A B a0 b0
theorem UniqueAdd.of_card_nonpos {G : Type u_1} [Add G] {A : } {B : } (hA : A.Nonempty) (hB : B.Nonempty) (hA1 : A.card 1) (hB1 : B.card 1) :
aA, bB, UniqueAdd A B a b
theorem UniqueMul.of_card_le_one {G : Type u_1} [Mul G] {A : } {B : } (hA : A.Nonempty) (hB : B.Nonempty) (hA1 : A.card 1) (hB1 : B.card 1) :
aA, bB, UniqueMul A B a b
theorem UniqueAdd.mt {G : Type u_1} [Add G] {A : } {B : } {a0 : G} {b0 : G} (h : UniqueAdd A B a0 b0) ⦃a : G ⦃b : G :
a Ab Ba a0 b b0a + b a0 + b0
theorem UniqueMul.mt {G : Type u_1} [Mul G] {A : } {B : } {a0 : G} {b0 : G} (h : UniqueMul A B a0 b0) ⦃a : G ⦃b : G :
a Ab Ba a0 b b0a * b a0 * b0
theorem UniqueAdd.subsingleton {G : Type u_1} [Add G] {A : } {B : } {a0 : G} {b0 : G} (h : UniqueAdd A B a0 b0) :
Subsingleton { ab : G × G // ab.1 A ab.2 B ab.1 + ab.2 = a0 + b0 }
abbrev UniqueAdd.subsingleton.match_1 {G : Type u_1} [Add G] {A : } {B : } {a0 : G} {b0 : G} (motive : { ab : G × G // ab.1 A ab.2 B ab.1 + ab.2 = a0 + b0 }Prop) :
∀ (x : { ab : G × G // ab.1 A ab.2 B ab.1 + ab.2 = a0 + b0 }), (∀ (_a' _b' : G) (ha' : (_a', _b').1 A) (hb' : (_a', _b').2 B) (ab' : (_a', _b').1 + (_a', _b').2 = a0 + b0), motive (_a', _b'), )motive x
Equations
• =
Instances For
theorem UniqueMul.subsingleton {G : Type u_1} [Mul G] {A : } {B : } {a0 : G} {b0 : G} (h : UniqueMul A B a0 b0) :
Subsingleton { ab : G × G // ab.1 A ab.2 B ab.1 * ab.2 = a0 * b0 }
theorem UniqueAdd.set_subsingleton {G : Type u_1} [Add G] {A : } {B : } {a0 : G} {b0 : G} (h : UniqueAdd A B a0 b0) :
{ab : G × G | ab.1 A ab.2 B ab.1 + ab.2 = a0 + b0}.Subsingleton
theorem UniqueMul.set_subsingleton {G : Type u_1} [Mul G] {A : } {B : } {a0 : G} {b0 : G} (h : UniqueMul A B a0 b0) :
{ab : G × G | ab.1 A ab.2 B ab.1 * ab.2 = a0 * b0}.Subsingleton
theorem UniqueAdd.iff_existsUnique {G : Type u_1} [Add G] {A : } {B : } {a0 : G} {b0 : G} (aA : a0 A) (bB : b0 B) :
UniqueAdd A B a0 b0 ∃! ab : G × G, ab A ×ˢ B ab.1 + ab.2 = a0 + b0
theorem UniqueMul.iff_existsUnique {G : Type u_1} [Mul G] {A : } {B : } {a0 : G} {b0 : G} (aA : a0 A) (bB : b0 B) :
UniqueMul A B a0 b0 ∃! ab : G × G, ab A ×ˢ B ab.1 * ab.2 = a0 * b0
abbrev UniqueAdd.iff_card_nonpos.match_1 {G : Type u_1} [Add G] {A : } {B : } {a0 : G} {b0 : G} (p2 : G × G) (motive : (p2.1 A p2.2 B) p2.1 + p2.2 = a0 + b0Prop) :
∀ (x : (p2.1 A p2.2 B) p2.1 + p2.2 = a0 + b0), (∀ (ha2 : p2.1 A) (hb2 : p2.2 B) (he2 : p2.1 + p2.2 = a0 + b0), motive )motive x
Equations
• =
Instances For
theorem UniqueAdd.iff_card_nonpos {G : Type u_1} [Add G] {A : } {B : } {a0 : G} {b0 : G} [] (ha0 : a0 A) (hb0 : b0 B) :
UniqueAdd A B a0 b0 (Finset.filter (fun (p : G × G) => p.1 + p.2 = a0 + b0) (A ×ˢ B)).card 1
theorem UniqueMul.iff_card_le_one {G : Type u_1} [Mul G] {A : } {B : } {a0 : G} {b0 : G} [] (ha0 : a0 A) (hb0 : b0 B) :
UniqueMul A B a0 b0 (Finset.filter (fun (p : G × G) => p.1 * p.2 = a0 * b0) (A ×ˢ B)).card 1
abbrev UniqueAdd.exists_iff_exists_existsUnique.match_2 {G : Type u_1} [Add G] {A : } {B : } (motive : (∃ (g : G), ∃! ab : G × G, ab A ×ˢ B ab.1 + ab.2 = g)Prop) :
∀ (x : ∃ (g : G), ∃! ab : G × G, ab A ×ˢ B ab.1 + ab.2 = g), (∀ (g : G) (h : ∃! ab : G × G, ab A ×ˢ B ab.1 + ab.2 = g), motive )motive x
Equations
• =
Instances For
abbrev UniqueAdd.exists_iff_exists_existsUnique.match_1 {G : Type u_1} [Add G] {A : } {B : } (motive : (∃ (a0 : G) (b0 : G), a0 A b0 B UniqueAdd A B a0 b0)Prop) :
∀ (x : ∃ (a0 : G) (b0 : G), 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 )motive x
Equations
• =
Instances For
theorem UniqueAdd.exists_iff_exists_existsUnique {G : Type u_1} [Add G] {A : } {B : } :
(∃ (a0 : G) (b0 : G), a0 A b0 B UniqueAdd A B a0 b0) ∃ (g : G), ∃! ab : G × G, ab A ×ˢ B ab.1 + ab.2 = g
theorem UniqueMul.exists_iff_exists_existsUnique {G : Type u_1} [Mul G] {A : } {B : } :
(∃ (a0 : G) (b0 : G), a0 A b0 B UniqueMul A B a0 b0) ∃ (g : G), ∃! ab : G × G, ab A ×ˢ B ab.1 * ab.2 = g
theorem UniqueAdd.addHom_preimage {G : Type u_1} {H : Type u_2} [Add G] [Add H] (f : AddHom G H) (hf : ) (a0 : G) (b0 : G) {A : } {B : } (u : UniqueAdd A B (f a0) (f b0)) :
UniqueAdd (A.preimage f ) (B.preimage f ) 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 : ) (a0 : G) (b0 : G) {A : } {B : } (u : UniqueMul A B (f a0) (f b0)) :
UniqueMul (A.preimage f ) (B.preimage f ) a0 b0

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

theorem UniqueAdd.of_addHom_image {G : Type u_1} {H : Type u_2} [Add G] [Add H] {A : } {B : } {a0 : G} {b0 : G} [] (f : AddHom G H) (hf : ∀ ⦃a b c d : G⦄, a + b = c + df a = f c f b = f da = c b = d) (h : UniqueAdd (Finset.image (f) A) (Finset.image (f) B) (f a0) (f b0)) :
UniqueAdd A B a0 b0
theorem UniqueMul.of_mulHom_image {G : Type u_1} {H : Type u_2} [Mul G] [Mul H] {A : } {B : } {a0 : G} {b0 : G} [] (f : G →ₙ* H) (hf : ∀ ⦃a b c d : G⦄, a * b = c * df a = f c f b = f da = c b = d) (h : UniqueMul (Finset.image (f) A) (Finset.image (f) B) (f a0) (f b0)) :
UniqueMul A B a0 b0
theorem UniqueAdd.addHom_image_iff {G : Type u_1} {H : Type u_2} [Add G] [Add H] {A : } {B : } {a0 : G} {b0 : G} [] (f : AddHom G H) (hf : ) :
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 : } {B : } {a0 : G} {b0 : G} [] (f : G →ₙ* H) (hf : ) :
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 : } {B : } {a0 : G} {b0 : G} (f : G H) (mul : ∀ (x y : G), f (x + y) = f x + f y) :
UniqueAdd () () (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 : } {B : } {a0 : G} {b0 : G} (f : G H) (mul : ∀ (x y : G), f (x * y) = f x * f y) :
UniqueMul () () (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 : } {B : } {a0 : G} {b0 : G} (h : UniqueAdd (Finset.map { toFun := AddOpposite.op, inj' := } B) (Finset.map { toFun := AddOpposite.op, inj' := } A) () ()) :
UniqueAdd A B a0 b0
theorem UniqueMul.of_mulOpposite {G : Type u_1} [Mul G] {A : } {B : } {a0 : G} {b0 : G} (h : UniqueMul (Finset.map { toFun := MulOpposite.op, inj' := } B) (Finset.map { toFun := MulOpposite.op, inj' := } A) () ()) :
UniqueMul A B a0 b0
theorem UniqueAdd.to_addOpposite {G : Type u_1} [Add G] {A : } {B : } {a0 : G} {b0 : G} (h : UniqueAdd A B a0 b0) :
UniqueAdd (Finset.map { toFun := AddOpposite.op, inj' := } B) (Finset.map { toFun := AddOpposite.op, inj' := } A) () ()
theorem UniqueMul.to_mulOpposite {G : Type u_1} [Mul G] {A : } {B : } {a0 : G} {b0 : G} (h : UniqueMul A B a0 b0) :
UniqueMul (Finset.map { toFun := MulOpposite.op, inj' := } B) (Finset.map { toFun := MulOpposite.op, inj' := } A) () ()
theorem UniqueAdd.iff_addOpposite {G : Type u_1} [Add G] {A : } {B : } {a0 : G} {b0 : G} :
UniqueAdd (Finset.map { toFun := AddOpposite.op, inj' := } B) (Finset.map { toFun := AddOpposite.op, inj' := } A) () () UniqueAdd A B a0 b0
theorem UniqueMul.iff_mulOpposite {G : Type u_1} [Mul G] {A : } {B : } {a0 : G} {b0 : G} :
UniqueMul (Finset.map { toFun := MulOpposite.op, inj' := } B) (Finset.map { toFun := MulOpposite.op, inj' := } A) () () UniqueMul A B a0 b0
theorem UniqueAdd.of_image_filter {G : Type u_1} {H : Type u_2} [Add G] [Add H] [] (f : AddHom G H) {A : } {B : } {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 : G) => f x = aH) A) (Finset.filter (fun (x : G) => 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] [] (f : G →ₙ* H) {A : } {B : } {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 : G) => f x = aH) A) (Finset.filter (fun (x : G) => f x = bH) B) aG bG) :
UniqueMul A B aG bG
class UniqueSums (G : Type u_1) [Add G] :

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.

• uniqueAdd_of_nonempty : ∀ {A B : }, A.NonemptyB.Nonemptya0A, b0B, 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

Instances
theorem UniqueSums.uniqueAdd_of_nonempty {G : Type u_1} [Add G] [self : ] {A : } {B : } :
A.NonemptyB.Nonemptya0A, b0B, 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

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

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.

• uniqueMul_of_nonempty : ∀ {A B : }, A.NonemptyB.Nonemptya0A, b0B, 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

Instances
theorem UniqueProds.uniqueMul_of_nonempty {G : Type u_1} [Mul G] [self : ] {A : } {B : } :
A.NonemptyB.Nonemptya0A, b0B, 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

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

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.

• uniqueAdd_of_one_lt_card : ∀ {A B : }, 1 < A.card * B.cardp1A ×ˢ B, p2A ×ˢ B, p1 p2 UniqueAdd A B p1.1 p1.2 UniqueAdd A B p2.1 p2.2

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

Instances
theorem TwoUniqueSums.uniqueAdd_of_one_lt_card {G : Type u_1} [Add G] [self : ] {A : } {B : } :
1 < A.card * B.cardp1A ×ˢ B, p2A ×ˢ B, p1 p2 UniqueAdd A B p1.1 p1.2 UniqueAdd A B p2.1 p2.2

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

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

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.

• uniqueMul_of_one_lt_card : ∀ {A B : }, 1 < A.card * B.cardp1A ×ˢ B, p2A ×ˢ B, p1 p2 UniqueMul A B p1.1 p1.2 UniqueMul A B p2.1 p2.2

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

Instances
theorem TwoUniqueProds.uniqueMul_of_one_lt_card {G : Type u_1} [Mul G] [self : ] {A : } {B : } :
1 < A.card * B.cardp1A ×ˢ B, p2A ×ˢ B, p1 p2 UniqueMul A B p1.1 p1.2 UniqueMul A B p2.1 p2.2

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

theorem uniqueAdd_of_twoUniqueAdd {G : Type u_1} [Add G] {A : } {B : } (h : 1 < A.card * B.cardp1A ×ˢ B, p2A ×ˢ B, p1 p2 UniqueAdd A B p1.1 p1.2 UniqueAdd A B p2.1 p2.2) (hA : A.Nonempty) (hB : B.Nonempty) :
aA, bB, UniqueAdd A B a b
theorem uniqueMul_of_twoUniqueMul {G : Type u_1} [Mul G] {A : } {B : } (h : 1 < A.card * B.cardp1A ×ˢ B, p2A ×ˢ B, p1 p2 UniqueMul A B p1.1 p1.2 UniqueMul A B p2.1 p2.2) (hA : A.Nonempty) (hB : B.Nonempty) :
aA, bB, UniqueMul A B a b
instance TwoUniqueSums.toUniqueSums (G : Type u_1) [Add G] [] :
Equations
• =
instance TwoUniqueProds.toUniqueProds (G : Type u_1) [Mul G] [] :
Equations
• =
Equations
• =
Equations
• =
instance Additive.instUniqueSumsOfUniqueProds {M : Type u_1} [Mul M] [] :
Equations
• =
Equations
• =
theorem UniqueSums.of_addHom {G : Type u} {H : Type v} [Add G] [Add H] (f : AddHom H G) (hf : ∀ ⦃a b c d : H⦄, a + b = c + df a = f c f b = f da = c b = d) [] :
theorem UniqueProds.of_mulHom {G : Type u} {H : Type v} [Mul G] [Mul H] (f : H →ₙ* G) (hf : ∀ ⦃a b c d : H⦄, a * b = c * df a = f c f b = f da = c b = d) [] :
theorem UniqueSums.of_injective_addHom {G : Type u} {H : Type v} [Add G] [Add H] (f : AddHom H G) (hf : ) :
theorem UniqueProds.of_injective_mulHom {G : Type u} {H : Type v} [Mul G] [Mul H] (f : H →ₙ* G) (hf : ) :
theorem AddEquiv.uniqueSums_iff {G : Type u} {H : Type v} [Add G] [Add H] (f : G ≃+ H) :

UniqueSums is preserved under additive equivalences.

theorem MulEquiv.uniqueProds_iff {G : Type u} {H : Type v} [Mul G] [Mul H] (f : G ≃* H) :

UniqueProd is preserved under multiplicative equivalences.

theorem UniqueSums.of_addOpposite {G : Type u} [Add G] (h : ) :
abbrev UniqueSums.of_addOpposite.match_1 {G : Type u_1} [Add G] :
∀ {A B : } (f : G Gᵃᵒᵖ) (motive : (a0, b0, UniqueAdd () () a0 b0)Prop) (x : a0, b0, UniqueAdd () () a0 b0), (∀ (y : Gᵃᵒᵖ) (yB : y ) (x : Gᵃᵒᵖ) (xA : x ) (hxy : UniqueAdd () () y x), motive )motive x
Equations
• =
Instances For
theorem UniqueProds.of_mulOpposite {G : Type u} [Mul G] (h : ) :
instance UniqueSums.instAddOpposite {G : Type u} [Add G] [h : ] :
Equations
• =
instance UniqueProds.instMulOpposite {G : Type u} [Mul G] [h : ] :
Equations
• =
theorem UniqueSums.toIsAddCancel {G : Type u} [Add G] [] :
theorem UniqueProds.toIsCancelMul {G : Type u} [Mul G] [] :

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

theorem UniqueSums.of_same {G : Type u_1} [] [] (h : ∀ {A : }, A.Nonemptya1A, a2A, UniqueAdd A A a1 a2) :
theorem UniqueProds.of_same {G : Type u_1} [] [] (h : ∀ {A : }, A.Nonemptya1A, a2A, UniqueMul A A a1 a2) :

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.

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].

instance UniqueSums.instForall {ι : Type u_2} (G : ιType u_1) [(i : ι) → Add (G i)] [∀ (i : ι), UniqueSums (G i)] :
UniqueSums ((i : ι) → G i)
Equations
• =
instance UniqueProds.instForall {ι : Type u_2} (G : ιType u_1) [(i : ι) → Mul (G i)] [∀ (i : ι), UniqueProds (G i)] :
UniqueProds ((i : ι) → G i)
Equations
• =
instance UniqueSums.instSum {G : Type u} {H : Type v} [Add G] [Add H] [] [] :
Equations
• =
instance UniqueProds.instProd {G : Type u} {H : Type v} [Mul G] [Mul H] [] [] :
Equations
• =
instance instUniqueSumsDFinsupp {ι : Type u_2} (G : ιType u_1) [(i : ι) → AddZeroClass (G i)] [∀ (i : ι), UniqueSums (G i)] :
UniqueSums (Π₀ (i : ι), G i)
Equations
• =
instance instUniqueSumsFinsupp {ι : Type u_1} {G : Type u_2} [] [] :
Equations
• =
theorem TwoUniqueSums.of_addHom {G : Type u} {H : Type v} [Add G] [Add H] (f : AddHom H G) (hf : ∀ ⦃a b c d : H⦄, a + b = c + df a = f c f b = f da = c b = d) [] :
theorem TwoUniqueProds.of_mulHom {G : Type u} {H : Type v} [Mul G] [Mul H] (f : H →ₙ* G) (hf : ∀ ⦃a b c d : H⦄, a * b = c * df a = f c f b = f da = c b = d) [] :
theorem TwoUniqueSums.of_injective_addHom {G : Type u} {H : Type v} [Add G] [Add H] (f : AddHom H G) (hf : ) :
theorem TwoUniqueProds.of_injective_mulHom {G : Type u} {H : Type v} [Mul G] [Mul H] (f : H →ₙ* G) (hf : ) :
theorem AddEquiv.twoUniqueSums_iff {G : Type u} {H : Type v} [Add G] [Add H] (f : G ≃+ H) :

TwoUniqueSums is preserved under additive equivalences.

theorem MulEquiv.twoUniqueProds_iff {G : Type u} {H : Type v} [Mul G] [Mul H] (f : G ≃* H) :

TwoUniqueProd is preserved under multiplicative equivalences.

instance TwoUniqueSums.instForall {ι : Type u_2} (G : ιType u_1) [(i : ι) → Add (G i)] [∀ (i : ι), TwoUniqueSums (G i)] :
TwoUniqueSums ((i : ι) → G i)
Equations
• =
instance TwoUniqueProds.instForall {ι : Type u_2} (G : ιType u_1) [(i : ι) → Mul (G i)] [∀ (i : ι), TwoUniqueProds (G i)] :
TwoUniqueProds ((i : ι) → G i)
Equations
• =
instance TwoUniqueSums.instSum {G : Type u} {H : Type v} [Add G] [Add H] [] [] :
Equations
• =
instance TwoUniqueProds.instProd {G : Type u} {H : Type v} [Mul G] [Mul H] [] [] :
Equations
• =
theorem TwoUniqueSums.of_addOpposite {G : Type u} [Add G] (h : ) :
theorem TwoUniqueProds.of_mulOpposite {G : Type u} [Mul G] (h : ) :
instance TwoUniqueSums.instAddOpposite {G : Type u} [Add G] [h : ] :
Equations
• =
instance TwoUniqueProds.instMulOpposite {G : Type u} [Mul G] [h : ] :
Equations
• =
@[instance 100]
instance TwoUniqueSums.of_covariant_right {G : Type u} [Add G] [] [] [CovariantClass G G (fun (x x_1 : G) => x + x_1) fun (x x_1 : G) => x < x_1] :

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.

Equations
• =
@[instance 100]
instance TwoUniqueProds.of_covariant_right {G : Type u} [Mul G] [] [] [CovariantClass G G (fun (x x_1 : G) => x * x_1) fun (x x_1 : G) => x < x_1] :

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.

Equations
• =
@[instance 100]
instance TwoUniqueSums.of_covariant_left {G : Type u} [Add G] [] [] [CovariantClass G G (Function.swap fun (x x_1 : G) => x + x_1) fun (x x_1 : G) => x < x_1] :

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.

Equations
• =
@[instance 100]
instance TwoUniqueProds.of_covariant_left {G : Type u} [Mul G] [] [] [CovariantClass G G (Function.swap fun (x x_1 : G) => x * x_1) fun (x x_1 : G) => x < x_1] :

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.

Equations
• =
@[deprecated UniqueProds.of_injective_mulHom]
theorem UniqueProds.mulHom_image_of_injective {G : Type u} {H : Type v} [Mul G] [Mul H] (f : H →ₙ* G) (hf : ) :

Alias of UniqueProds.of_injective_mulHom.

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

Alias of UniqueSums.of_injective_addHom.

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

Alias of MulEquiv.uniqueProds_iff.

UniqueProd is preserved under multiplicative equivalences.

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

Alias of AddEquiv.uniqueSums_iff.

UniqueSums is preserved under additive equivalences.

@[deprecated TwoUniqueProds.of_injective_mulHom]
theorem TwoUniqueProds.mulHom_image_of_injective {G : Type u} {H : Type v} [Mul G] [Mul H] (f : H →ₙ* G) (hf : ) :

Alias of TwoUniqueProds.of_injective_mulHom.

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

Alias of TwoUniqueSums.of_injective_addHom.

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

Alias of MulEquiv.twoUniqueProds_iff.

TwoUniqueProd is preserved under multiplicative equivalences.

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

Alias of AddEquiv.twoUniqueSums_iff.

TwoUniqueSums is preserved under additive equivalences.

instance instTwoUniqueSumsDFinsupp {ι : Type u_2} (G : ιType u_1) [(i : ι) → AddZeroClass (G i)] [∀ (i : ι), TwoUniqueSums (G i)] :
TwoUniqueSums (Π₀ (i : ι), G i)
Equations
• =
instance instTwoUniqueSumsFinsupp {ι : Type u_1} {G : Type u_2} [] [] :
Equations
• =
instance instTwoUniqueSumsOfModuleRat {G : Type u} [] [] :

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.

Equations
• =
instance FreeMonoid.instTwoUniqueProds {κ : Type u_1} :

Any FreeMonoid has the TwoUniqueProds property.

Equations
• =

Any FreeAddMonoid has the TwoUniqueSums property.

Equations
• =