Theorems · Definition · group theory

DirectSum.IsInternal.chooseDecomposition

{ι : 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.IsInternal ℳ → DirectSum.Decomposition ℳ

Noncomputably conjure a decomposition instance from a DirectSum.IsInternal proof.

Defined in: Mathlib.Algebra.DirectSum.Decomposition
Cited by: 0 results in Mathlib
Foundations: Depth 88 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: DecidableEq AddCommMonoid SetLike AddSubmonoidClass

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites9

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

DFunLike.coeproof · cited by 62,936
AddCommMonoidstatement and proof · cited by 12,281
Equiv.symmproof · cited by 3,681
SetLikestatement and proof · cited by 1,084
AddSubmonoidClassstatement and proof · cited by 346
Equiv.ofBijectiveproof · cited by 70
DirectSum.IsInternalstatement and proof · cited by 65
DirectSum.Decompositionstatement · cited by 57
DirectSum.coeAddMonoidHomproof · cited by 8

Cited by0

Results whose statement or proof uses this declaration.

Nothing cites this yet.