Theorems · Definition · group theory

DirectSum.Decomposition.noConfusion

{P : Sort u} →
  {ι : Type u_1} →
    {M : Type u_3} →
      {σ : Type u_4} →
        {inst : DecidableEq ι} →
          {inst_1 : AddCommMonoid M} →
            {inst_2 : SetLike σ M} →
              {inst_3 : AddSubmonoidClass σ M} →
                {ℳ : ι → σ} →
                  {t : DirectSum.Decomposition ℳ} →
                    {ι' : Type u_1} →
                      {M' : Type u_3} →
                        {σ' : Type u_4} →
                          {inst' : DecidableEq ι'} →
                            {inst'_1 : AddCommMonoid M'} →
                              {inst'_2 : SetLike σ' M'} →
                                {inst'_3 : AddSubmonoidClass σ' M'} →
                                  {ℳ' : ι' → σ'} →
                                    {t' : DirectSum.Decomposition ℳ'} →
                                      ι = ι' →
                                        M = M' →
                                          σ = σ' →
                                            inst ≍ inst' →
                                              inst_1 ≍ inst'_1 →
                                                inst_2 ≍ inst'_2 →
                                                  inst_3 ≍ inst'_3 →
                                                    ℳ ≍ ℳ' → t ≍ t' → DirectSum.Decomposition.noConfusionType P t t'

Defined in

Mathlib.Algebra.DirectSum.Decomposition

Cited by

0 results in Mathlib

Foundations

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