Theorems · Definition · general algebraic systems

DFinsupp.noConfusionType

Sort u_1 →
  {ι : Type u} →
    {β : ι → Type v} →
      [inst : (i : ι) → Zero (β i)] →
        DFinsupp β → {ι' : Type u} → {β' : ι' → Type v} → [inst' : (i : ι') → Zero (β' i)] → DFinsupp β' → Sort u_1

Defined in: Mathlib.Data.DFinsupp.Defs
Cited by: 0 results in Mathlib
Foundations: Depth 18 from the axioms · uses propext
Assumes: Zero Zero

Mathlib docs Source Loogle LeanSearch

Around this declaration

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

Cites4

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

Multisetproof · cited by 2,627
DFinsuppstatement and proof · cited by 694
Truncproof · cited by 39
DFinsupp.casesOnproof · cited by 6

Cited by1

Results whose statement or proof uses this declaration.

DFinsupp.noConfusionstatement · cited by 0