finsuppLEquivDirectSum — Mathlib

English

The finitely supported functions ι →₀ M are linearly equivalent to the direct sum ⨁_ι M indexed by ι.

Русский

Конечноподдерживаемые функции ι →₀ M линейно эквивалентны прямой сумме ⨁_ι M индексируемой по ι.

LaTeX

$$$(ι \to_0 M) \simeq_{R} \bigoplus_{i} M$$$

Lean4

/-- The finitely supported functions `ι →₀ M` are in linear equivalence with the direct sum of
copies of M indexed by ι. -/
def finsuppLEquivDirectSum : (ι →₀ M) ≃ₗ[R] ⨁ _ : ι, M :=
  haveI : ∀ m : M, Decidable (m ≠ 0) := Classical.decPred _
  finsuppLequivDFinsupp R

Похожие утверждения