Theorems · Definition · commutative algebra

finsuppLEquivDirectSum

(R : Type u) →
  (M : Type v) →
    [inst : Semiring R] →
      [inst_1 : AddCommMonoid M] →
        [inst_2 : Module R M] → (ι : Type u_1) → [DecidableEq ι] → (ι →₀ M) ≃ₗ[R] DirectSum ι fun x => M

The finitely supported functions ι →₀ M are in linear equivalence with the direct sum of copies of M indexed by ι.

Defined in

Mathlib.Algebra.DirectSum.Finsupp

Cited by

10 results in Mathlib

Foundations

Depth 85 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

SemiringAddCommMonoidModuleDecidableEq