English
For a finite set s in a commutative group, the span mulSpan(s) consists of all finite products of the form ∏_{a∈s} a^{ε(a)} where ε ∈ {−1,0,1}^s.
Русский
Для конечного множества s в коммутативной группе спан mulSpan(s) состоит из всех конечных произведений вида ∏_{a∈s} a^{ε(a)}, где ε ∈ {−1,0,1}^s.
LaTeX
$$$\text{mulSpan}(s) = \{ \prod_{a \in s} a^{\varepsilon(a)} : \varepsilon \in \{-1,0,1\}^s \}$$$
Lean4
/-- The span of a finset `s` is the finset of elements of the form `∏ a ∈ s, a ^ ε a` where
`ε ∈ {-1, 0, 1} ^ s`.
This is an analog of the linear span in a vector space, but with the "scalars" restricted to
`0` and `±1`. -/
@[to_additive /-- The span of a finset `s` is the finset of elements of the form `∑ a ∈ s, ε a • a`
where `ε ∈ {-1, 0, 1} ^ s`.
This is an analog of the linear span in a vector space, but with the "scalars" restricted to
`0` and `±1`. -/
]
def mulSpan (s : Finset α) : Finset α :=
(Fintype.piFinset fun _a ↦ ({-1, 0, 1} : Finset ℤ)).image fun ε ↦ ∏ a ∈ s, a ^ ε a
