English
There is a linear equivalence lequivProdDirectSum between a direct sum over Option-indexed α_i and the product of α none with the direct sum over some indices, separating the none-index from the some-index parts (with respect to a choice of bases).
Русский
Существует линейная эквивалентность между прямой суммой по индексам Option и произведением α none на прямую сумму по some индексам, отделяющая компонент none от компонент some (с выбором баз).
LaTeX
$$$\text{lequivProdDirectSum} : (\bigoplus i, \alpha i) \simeq_\!R \alpha(\text none) \times (\bigoplus i, \alpha (\text some i)).$$$
Lean4
/-- Linear isomorphism obtained by separating the term of index `none` of a direct sum over
`Option ι`. -/
@[simps]
noncomputable def lequivProdDirectSum : (⨁ i, α i) ≃ₗ[R] α none × ⨁ i, α (some i) :=
{ addEquivProdDirectSum with map_smul' := DFinsupp.equivProdDFinsupp_smul }
