Unique products and related notions #
A group G
has unique products if for any two non-empty finite subsets A, B ⊂ G⊂ G
, there is an
element g ∈ A * B∈ 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
.
Here you can see several examples of Types that have UniqueSums/Prods
(infer_instance
uses covariants.to_uniqueProds
and covariants.to_uniqueSums
).
import Mathlib.Data.Real.Basic
import Mathlib.Data.PNat.Basic
import Mathlib.Algebra.Group.UniqueProds
example : UniqueSums ℕ := by infer_instance
example : UniqueSums ℕ+ := by infer_instance
example : UniqueSums ℤ := by infer_instance
example : UniqueSums ℚ := by infer_instance
example : UniqueSums ℝ := by infer_instance
example : UniqueProds ℕ+ := by infer_instance
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
.
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
- One or more equations did not get rendered due to their size.
Equations
- UniqueAdd.exists_iff_exists_existsUnique.match_2 motive x h_1 = Exists.casesOn x fun w h => h_1 w h
UniqueAdd
is preserved by inverse images under injective, additive maps.
UniqueMul
is preserved by inverse images under injective, multiplicative maps.
UniqueAdd
is preserved under additive maps that are injective.
See UniqueAdd.addHom_map_iff
for a version with swapped bundling.
Unique_Mul
is preserved under multiplicative maps that are injective.
See UniqueMul.mulHom_map_iff
for a version with swapped bundling.
UniqueAdd
is preserved under embeddings that are additive.
See UniqueAdd.addHom_image_iff
for a version with swapped bundling.
UniqueMul
is preserved under embeddings that are multiplicative.
See UniqueMul.mulHom_image_iff
for a version with swapped bundling.
For
A B
two nonempty finite sets, there always exista0 ∈ A, b0 ∈ B∈ A, b0 ∈ B∈ B
such thatUniqueAdd A B a0 b0
uniqueAdd_of_nonempty : ∀ {A B : Finset G}, Finset.Nonempty A → Finset.Nonempty B → ∃ a0, a0 ∈ A ∧ ∃ b0, b0 ∈ B ∧ UniqueAdd A B a0 b0
Let G
be a Type with addition. UniqueSums G
asserts that any two non-empty
finite subsets of A
have the UniqueAdd
property, with respect to some element of their
sum A + B
.
Instances
For
A B
two nonempty finite sets, there always exista0 ∈ A, b0 ∈ B∈ A, b0 ∈ B∈ B
such thatUniqueMul A B a0 b0
uniqueMul_of_nonempty : ∀ {A B : Finset G}, Finset.Nonempty A → Finset.Nonempty B → ∃ a0, a0 ∈ A ∧ ∃ b0, b0 ∈ B ∧ 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
.
Instances
This instance asserts that if A
has an addition, a linear order, and addition
is 'very monotone', then A
also has UniqueSums
.
Equations
- (_ : UniqueSums A) = (_ : UniqueSums A)
This instance asserts that if A
has a multiplication, a linear order, and multiplication
is 'very monotone', then A
also has UniqueProds
.