Theorems · Definition · group theory

DirectSum.decompose

{ι : Type u_1} →
  {M : Type u_3} →
    {σ : Type u_4} →
      [inst : DecidableEq ι] →
        [inst_1 : AddCommMonoid M] →
          [inst_2 : SetLike σ M] →
            [inst_3 : AddSubmonoidClass σ M] →
              (ℳ : ι → σ) → [DirectSum.Decomposition ℳ] → M ≃ DirectSum ι fun i => ↥(ℳ i)

If M is graded by ι with degree i component ℳ i, then it is isomorphic as to a direct sum of components. This is the canonical spelling of the decompose' field.

Defined in

Mathlib.Algebra.DirectSum.Decomposition

Cited by

93 results in Mathlib

Foundations

Depth 87 from the axioms, rests on 2,060 definitions · uses propext, Classical.choice, Quot.sound

Assumes

DecidableEqAddCommMonoidSetLikeAddSubmonoidClassDirectSum.Decomposition