# 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.Basic

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

## Use in `(Add)MonoidAlgebra`s #

`UniqueProds/Sums` allow to decouple certain arguments about `(Add)MonoidAlgebra`s 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.

source
def UniqueMul {G : Type u_1} [Mul G] (A B : Finset G) (a0 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`.

Equations

- UniqueMul A B a0 b0 = ∀ ⦃a b : G⦄, a ∈ A → b ∈ B → a * b = a0 * b0 → a = a0 ∧ b = b0

Instances For

source
def UniqueAdd {G : Type u_1} [Add G] (A B : Finset G) (a0 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`.

Equations

- UniqueAdd A B a0 b0 = ∀ ⦃a b : G⦄, a ∈ A → b ∈ B → a + b = a0 + b0 → a = a0 ∧ b = b0

Instances For

source
theorem UniqueMul.mono {G : Type u_1} [Mul G] {A B : Finset G} {a0 b0 : G} {A' B' : Finset G} (hA : A ⊆ A') (hB : B ⊆ B') (h : UniqueMul A' B' a0 b0) :
UniqueMul A B a0 b0
source
theorem UniqueAdd.mono {G : Type u_1} [Add G] {A B : Finset G} {a0 b0 : G} {A' B' : Finset G} (hA : A ⊆ A') (hB : B ⊆ B') (h : UniqueAdd A' B' a0 b0) :
UniqueAdd A B a0 b0
source
@[simp]
theorem UniqueMul.of_subsingleton {G : Type u_1} [Mul G] {A B : Finset G} {a0 b0 : G} [Subsingleton G] :
UniqueMul A B a0 b0
source
@[simp]
theorem UniqueAdd.of_subsingleton {G : Type u_1} [Add G] {A B : Finset G} {a0 b0 : G} [Subsingleton G] :
UniqueAdd A B a0 b0
source
theorem UniqueMul.of_card_le_one {G : Type u_1} [Mul G] {A B : Finset G} (hA : A.Nonempty) (hB : B.Nonempty) (hA1 : A.card ≤ 1) (hB1 : B.card ≤ 1) :
∃ a ∈ A, ∃ b ∈ B, UniqueMul A B a b
source
theorem UniqueAdd.of_card_le_one {G : Type u_1} [Add G] {A B : Finset G} (hA : A.Nonempty) (hB : B.Nonempty) (hA1 : A.card ≤ 1) (hB1 : B.card ≤ 1) :
∃ a ∈ A, ∃ b ∈ B, UniqueAdd A B a b
source
theorem UniqueMul.mt {G : Type u_1} [Mul G] {A B : Finset G} {a0 b0 : G} (h : UniqueMul A B a0 b0) ⦃a b : G⦄ :
a ∈ A → b ∈ B → a ≠ a0 ∨ b ≠ b0 → a * b ≠ a0 * b0
source
theorem UniqueAdd.mt {G : Type u_1} [Add G] {A B : Finset G} {a0 b0 : G} (h : UniqueAdd A B a0 b0) ⦃a b : G⦄ :
a ∈ A → b ∈ B → a ≠ a0 ∨ b ≠ b0 → a + b ≠ a0 + b0
source
theorem UniqueMul.subsingleton {G : Type u_1} [Mul G] {A B : Finset G} {a0 b0 : G} (h : UniqueMul A B a0 b0) :
Subsingleton { ab : G × G // ab.1 ∈ A ∧ ab.2 ∈ B ∧ ab.1 * ab.2 = a0 * b0 }
source
theorem UniqueAdd.subsingleton {G : Type u_1} [Add G] {A B : Finset G} {a0 b0 : G} (h : UniqueAdd A B a0 b0) :
Subsingleton { ab : G × G // ab.1 ∈ A ∧ ab.2 ∈ B ∧ ab.1 + ab.2 = a0 + b0 }
source
theorem UniqueMul.set_subsingleton {G : Type u_1} [Mul G] {A B : Finset G} {a0 b0 : G} (h : UniqueMul A B a0 b0) :
{ab : G × G | ab.1 ∈ A ∧ ab.2 ∈ B ∧ ab.1 * ab.2 = a0 * b0}.Subsingleton
source
theorem UniqueAdd.set_subsingleton {G : Type u_1} [Add G] {A B : Finset G} {a0 b0 : G} (h : UniqueAdd A B a0 b0) :
{ab : G × G | ab.1 ∈ A ∧ ab.2 ∈ B ∧ ab.1 + ab.2 = a0 + b0}.Subsingleton
source
theorem UniqueMul.iff_existsUnique {G : Type u_1} [Mul G] {A B : Finset G} {a0 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
source
theorem UniqueAdd.iff_existsUnique {G : Type u_1} [Add G] {A B : Finset G} {a0 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
source
theorem UniqueMul.iff_card_le_one {G : Type u_1} [Mul G] {A B : Finset G} {a0 b0 : G} [DecidableEq G] (ha0 : a0 ∈ A) (hb0 : b0 ∈ B) :
UniqueMul A B a0 b0 ↔ {p ∈ A ×ˢ B | p.1 * p.2 = a0 * b0}.card ≤ 1
source
theorem UniqueAdd.iff_card_le_one {G : Type u_1} [Add G] {A B : Finset G} {a0 b0 : G} [DecidableEq G] (ha0 : a0 ∈ A) (hb0 : b0 ∈ B) :
UniqueAdd A B a0 b0 ↔ {p ∈ A ×ˢ B | p.1 + p.2 = a0 + b0}.card ≤ 1
source
theorem UniqueMul.exists_iff_exists_existsUnique {G : Type u_1} [Mul G] {A B : Finset G} :
(∃ (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
source
theorem UniqueAdd.exists_iff_exists_existsUnique {G : Type u_1} [Add G] {A B : Finset G} :
(∃ (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
source
theorem UniqueMul.mulHom_preimage {G : Type u_1} {H : Type u_2} [Mul G] [Mul H] (f : G →ₙ* H) (hf : Function.Injective ⇑f) (a0 b0 : G) {A B : Finset H} (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.

source
theorem UniqueAdd.addHom_preimage {G : Type u_1} {H : Type u_2} [Add G] [Add H] (f : G →ₙ+ H) (hf : Function.Injective ⇑f) (a0 b0 : G) {A B : Finset H} (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.

source
theorem UniqueMul.of_mulHom_image {G : Type u_1} {H : Type u_2} [Mul G] [Mul H] {A B : Finset G} {a0 b0 : G} [DecidableEq H] (f : G →ₙ* H) (hf : ∀ ⦃a b c d : G⦄, a * b = c * d → f a = f c ∧ f b = f d → a = c ∧ b = d) (h : UniqueMul (Finset.image (⇑f) A) (Finset.image (⇑f) B) (f a0) (f b0)) :
UniqueMul A B a0 b0
source
theorem UniqueAdd.of_addHom_image {G : Type u_1} {H : Type u_2} [Add G] [Add H] {A B : Finset G} {a0 b0 : G} [DecidableEq H] (f : G →ₙ+ H) (hf : ∀ ⦃a b c d : G⦄, a + b = c + d → f a = f c ∧ f b = f d → a = c ∧ b = d) (h : UniqueAdd (Finset.image (⇑f) A) (Finset.image (⇑f) B) (f a0) (f b0)) :
UniqueAdd A B a0 b0
source
theorem UniqueMul.mulHom_image_iff {G : Type u_1} {H : Type u_2} [Mul G] [Mul H] {A B : Finset G} {a0 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.

source
theorem UniqueAdd.addHom_image_iff {G : Type u_1} {H : Type u_2} [Add G] [Add H] {A B : Finset G} {a0 b0 : G} [DecidableEq H] (f : 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.

source
theorem UniqueMul.mulHom_map_iff {G : Type u_1} {H : Type u_2} [Mul G] [Mul H] {A B : Finset G} {a0 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.

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

source
theorem UniqueMul.of_mulOpposite {G : Type u_1} [Mul G] {A B : Finset G} {a0 b0 : G} (h : 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
source
theorem UniqueAdd.of_addOpposite {G : Type u_1} [Add G] {A B : Finset G} {a0 b0 : G} (h : 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
source
theorem UniqueMul.to_mulOpposite {G : Type u_1} [Mul G] {A B : Finset G} {a0 b0 : G} (h : UniqueMul A B a0 b0) :
UniqueMul (Finset.map { toFun := MulOpposite.op, inj' := ⋯ } B) (Finset.map { toFun := MulOpposite.op, inj' := ⋯ } A) (MulOpposite.op b0) (MulOpposite.op a0)
source
theorem UniqueAdd.to_addOpposite {G : Type u_1} [Add G] {A B : Finset G} {a0 b0 : G} (h : UniqueAdd A B a0 b0) :
UniqueAdd (Finset.map { toFun := AddOpposite.op, inj' := ⋯ } B) (Finset.map { toFun := AddOpposite.op, inj' := ⋯ } A) (AddOpposite.op b0) (AddOpposite.op a0)
source
theorem UniqueMul.iff_mulOpposite {G : Type u_1} [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
source
theorem UniqueAdd.iff_addOpposite {G : Type u_1} [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
source
theorem UniqueMul.of_image_filter {G : Type u_1} {H : Type u_2} [Mul G] [Mul H] [DecidableEq H] (f : G →ₙ* H) {A B : Finset G} {aG bG : G} {aH bH : H} (hae : f aG = aH) (hbe : f bG = bH) (huH : UniqueMul (Finset.image (⇑f) A) (Finset.image (⇑f) B) aH bH) (huG : UniqueMul ({a ∈ A | f a = aH}) ({b ∈ B | f b = bH}) aG bG) :
UniqueMul A B aG bG
source
theorem UniqueAdd.of_image_filter {G : Type u_1} {H : Type u_2} [Add G] [Add H] [DecidableEq H] (f : G →ₙ+ H) {A B : Finset G} {aG bG : G} {aH bH : H} (hae : f aG = aH) (hbe : f bG = bH) (huH : UniqueAdd (Finset.image (⇑f) A) (Finset.image (⇑f) B) aH bH) (huG : UniqueAdd ({a ∈ A | f a = aH}) ({b ∈ B | f b = bH}) aG bG) :
UniqueAdd A B aG bG
source
class UniqueSums (G : Type u_1) [Add G] :
Prop

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 : Finset G} : A.Nonempty → B.Nonempty → ∃ a0 ∈ A, ∃ 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`

Instances

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

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 : Finset G} : A.Nonempty → B.Nonempty → ∃ a0 ∈ A, ∃ 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`

Instances

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

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 : 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

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

Instances

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

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 : 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

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

Instances

source
theorem uniqueMul_of_twoUniqueMul {G : Type u_1} [Mul G] {A B : Finset G} (h : 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) (hA : A.Nonempty) (hB : B.Nonempty) :
∃ a ∈ A, ∃ b ∈ B, UniqueMul A B a b
source
theorem uniqueAdd_of_twoUniqueAdd {G : Type u_1} [Add G] {A B : Finset G} (h : 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) (hA : A.Nonempty) (hB : B.Nonempty) :
∃ a ∈ A, ∃ b ∈ B, UniqueAdd A B a b
source
instance TwoUniqueProds.toUniqueProds (G : Type u_1) [Mul G] [TwoUniqueProds G] :
UniqueProds G
source
instance TwoUniqueSums.toUniqueSums (G : Type u_1) [Add G] [TwoUniqueSums G] :
UniqueSums G
source
instance Multiplicative.instUniqueProdsOfUniqueSums {M : Type u_1} [Add M] [UniqueSums M] :
UniqueProds (Multiplicative M)
source
instance Multiplicative.instTwoUniqueProdsOfTwoUniqueSums {M : Type u_1} [Add M] [TwoUniqueSums M] :
TwoUniqueProds (Multiplicative M)
source
instance Additive.instUniqueSumsOfUniqueProds {M : Type u_1} [Mul M] [UniqueProds M] :
UniqueSums (Additive M)
source
instance Additive.instTwoUniqueSumsOfTwoUniqueProds {M : Type u_1} [Mul M] [TwoUniqueProds M] :
TwoUniqueSums (Additive M)
source
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 * d → f a = f c ∧ f b = f d → a = c ∧ b = d) [UniqueProds G] :
UniqueProds H
source
theorem UniqueSums.of_addHom {G : Type u} {H : Type v} [Add G] [Add H] (f : H →ₙ+ G) (hf : ∀ ⦃a b c d : H⦄, a + b = c + d → f a = f c ∧ f b = f d → a = c ∧ b = d) [UniqueSums G] :
UniqueSums H
source
theorem UniqueProds.of_injective_mulHom {G : Type u} {H : Type v} [Mul G] [Mul H] (f : H →ₙ* G) (hf : Function.Injective ⇑f) :
UniqueProds G → UniqueProds H
source
theorem UniqueSums.of_injective_addHom {G : Type u} {H : Type v} [Add G] [Add H] (f : H →ₙ+ G) (hf : Function.Injective ⇑f) :
UniqueSums G → UniqueSums H
source
theorem MulEquiv.uniqueProds_iff {G : Type u} {H : Type v} [Mul G] [Mul H] (f : G ≃* H) :
UniqueProds G ↔ UniqueProds H

`UniqueProd` is preserved under multiplicative equivalences.

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

`UniqueSums` is preserved under additive equivalences.

source
theorem UniqueProds.of_mulOpposite {G : Type u} [Mul G] (h : UniqueProds G ᵐᵒᵖ) :
UniqueProds G
source
theorem UniqueSums.of_addOpposite {G : Type u} [Add G] (h : UniqueSums G ᵃᵒᵖ) :
UniqueSums G
source
instance UniqueProds.instMulOpposite {G : Type u} [Mul G] [h : UniqueProds G] :
UniqueProds G ᵐᵒᵖ
source
instance UniqueSums.instAddOpposite {G : Type u} [Add G] [h : UniqueSums G] :
UniqueSums G ᵃᵒᵖ
source
theorem UniqueProds.toIsCancelMul {G : Type u} [Mul G] [UniqueProds G] :
IsCancelMul G
source
theorem UniqueSums.toIsCancelAdd {G : Type u} [Add G] [UniqueSums G] :
IsCancelAdd G

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

source
theorem UniqueProds.of_same {G : Type u_1} [Semigroup G] [IsCancelMul G] (h : ∀ {A : Finset G}, A.Nonempty → ∃ a1 ∈ A, ∃ a2 ∈ A, UniqueMul A A a1 a2) :
UniqueProds G

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

source
theorem UniqueSums.of_same {G : Type u_1} [AddSemigroup G] [IsCancelAdd G] (h : ∀ {A : Finset G}, A.Nonempty → ∃ a1 ∈ A, ∃ a2 ∈ A, UniqueAdd A A a1 a2) :
UniqueSums G
source
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].

source
theorem UniqueSums.toTwoUniqueSums_of_addGroup {G : Type u_1} [AddGroup G] [UniqueSums G] :
TwoUniqueSums G
source
instance UniqueProds.instForall {ι : Type u_2} (G : ι → Type u_1) [(i : ι) → Mul (G i)] [∀ (i : ι), UniqueProds (G i)] :
UniqueProds ((i : ι) → G i)
source
instance UniqueSums.instForall {ι : Type u_2} (G : ι → Type u_1) [(i : ι) → Add (G i)] [∀ (i : ι), UniqueSums (G i)] :
UniqueSums ((i : ι) → G i)
source
instance Prod.instUniqueProds {G : Type u} {H : Type v} [Mul G] [Mul H] [UniqueProds G] [UniqueProds H] :
UniqueProds (G × H)
source
instance Prod.instUniqueSums {G : Type u} {H : Type v} [Add G] [Add H] [UniqueSums G] [UniqueSums H] :
UniqueSums (G × H)
source
instance instUniqueSumsDFinsupp {ι : Type u_2} (G : ι → Type u_1) [(i : ι) → AddZeroClass (G i)] [∀ (i : ι), UniqueSums (G i)] :
UniqueSums (Π₀ (i : ι), G i)
source
instance instUniqueSumsFinsupp {ι : Type u_1} {G : Type u_2} [AddZeroClass G] [UniqueSums G] :
UniqueSums (ι →₀ G)
source
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 * d → f a = f c ∧ f b = f d → a = c ∧ b = d) [TwoUniqueProds G] :
TwoUniqueProds H
source
theorem TwoUniqueSums.of_addHom {G : Type u} {H : Type v} [Add G] [Add H] (f : H →ₙ+ G) (hf : ∀ ⦃a b c d : H⦄, a + b = c + d → f a = f c ∧ f b = f d → a = c ∧ b = d) [TwoUniqueSums G] :
TwoUniqueSums H
source
theorem TwoUniqueProds.of_injective_mulHom {G : Type u} {H : Type v} [Mul G] [Mul H] (f : H →ₙ* G) (hf : Function.Injective ⇑f) :
TwoUniqueProds G → TwoUniqueProds H
source
theorem TwoUniqueSums.of_injective_addHom {G : Type u} {H : Type v} [Add G] [Add H] (f : H →ₙ+ G) (hf : Function.Injective ⇑f) :
TwoUniqueSums G → TwoUniqueSums H
source
theorem MulEquiv.twoUniqueProds_iff {G : Type u} {H : Type v} [Mul G] [Mul H] (f : G ≃* H) :
TwoUniqueProds G ↔ TwoUniqueProds H

`TwoUniqueProd` is preserved under multiplicative equivalences.

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

`TwoUniqueSums` is preserved under additive equivalences.

source
instance TwoUniqueProds.instForall {ι : Type u_2} (G : ι → Type u_1) [(i : ι) → Mul (G i)] [∀ (i : ι), TwoUniqueProds (G i)] :
TwoUniqueProds ((i : ι) → G i)
source
instance TwoUniqueSums.instForall {ι : Type u_2} (G : ι → Type u_1) [(i : ι) → Add (G i)] [∀ (i : ι), TwoUniqueSums (G i)] :
TwoUniqueSums ((i : ι) → G i)
source
instance Prod.instTwoUniqueProds {G : Type u} {H : Type v} [Mul G] [Mul H] [TwoUniqueProds G] [TwoUniqueProds H] :
TwoUniqueProds (G × H)
source
instance Prod.instTwoUniqueSums {G : Type u} {H : Type v} [Add G] [Add H] [TwoUniqueSums G] [TwoUniqueSums H] :
TwoUniqueSums (G × H)
source
theorem TwoUniqueProds.of_mulOpposite {G : Type u} [Mul G] (h : TwoUniqueProds G ᵐᵒᵖ) :
TwoUniqueProds G
source
theorem TwoUniqueSums.of_addOpposite {G : Type u} [Add G] (h : TwoUniqueSums G ᵃᵒᵖ) :
TwoUniqueSums G
source
instance TwoUniqueProds.instMulOpposite {G : Type u} [Mul G] [h : TwoUniqueProds G] :
TwoUniqueProds G ᵐᵒᵖ
source
instance TwoUniqueSums.instAddOpposite {G : Type u} [Add G] [h : TwoUniqueSums G] :
TwoUniqueSums G ᵃᵒᵖ
source
@[instance 100]
instance TwoUniqueProds.of_covariant_right {G : Type u} [Mul G] [IsRightCancelMul G] [LinearOrder G] [MulLeftStrictMono G] :
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`.

source
@[instance 100]
instance TwoUniqueSums.of_covariant_right {G : Type u} [Add G] [IsRightCancelAdd G] [LinearOrder G] [AddLeftStrictMono G] :
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`.

source
@[instance 100]
instance TwoUniqueProds.of_covariant_left {G : Type u} [Mul G] [IsLeftCancelMul G] [LinearOrder G] [MulRightStrictMono G] :
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`.

source
@[instance 100]
instance TwoUniqueSums.of_covariant_left {G : Type u} [Add G] [IsLeftCancelAdd G] [LinearOrder G] [AddRightStrictMono G] :
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`.

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