Structures · Algebra

DirectSum.Decomposition

A decomposition is an equivalence between an additive monoid M and a direct sum of additive submonoids ℳ i of that M, such that the "recomposition" is canonical. This definition also works for additive groups and modules. This is a version of DirectSum.IsInternal which comes with a constructive inverse to the canonical "recomposition" rather than just a proof that the "recomposition" is bijective. Often it is easier to construct a term of this type via Decomposition.ofAddHom or Decomposition.ofLinearMap.

Defined in

Mathlib.Algebra.DirectSum.Decomposition

Shape

One type argument · adds decompose', left_inv, right_inv