English
A subset s of a commutative group α is multiplicatively dissociated if the map t ↦ ∏ x ∈ t x, from finite subsets t with t ⊆ s, to α, is injective.
Русский
Подмножество s в коммутативной группе α называется мульти-расщепленным (MulDissociated), если отображение t ↦ ∏ x∈t x от конечных подмножеств t ⊆ s в α инъективно.
LaTeX
$$$$ \operatorname{MulDissociated}(s) \;\equiv\; \{t : \mathrm{Finset}\;\alpha \mid t \subseteq s\} \mathrm{InjOn}\left(\lambda t, \prod_{x\in t} x\right). $$$$
Lean4
/-- A set is dissociated iff all its finite subsets have different products.
This is an analog of linear independence in a vector space, but with the "scalars" restricted to
`0` and `±1`. -/
@[to_additive /-- A set is dissociated iff all its finite subsets have different sums.
This is an analog of linear independence in a vector space, but with the "scalars" restricted to
`0` and `±1`. -/
]
def MulDissociated (s : Set α) : Prop :=
{t : Finset α | ↑t ⊆ s}.InjOn (∏ x ∈ ·, x)
