Theorems · Theorem · general algebraic systems

DFinsupp.single_eq_of_sigma_eq

∀ {ι : Type u} {β : ι → Type v} [inst : (i : ι) → Zero (β i)] [inst_1 : DecidableEq ι] {i j : ι} {xi : β i} {xj : β j},
  ⟨i, xi⟩ = ⟨j, xj⟩ → (fun₀ | i => xi) = fun₀ | j => xj

Equality of sigma types is sufficient (but not necessary) to show equality of DFinsupps.

Defined in: Mathlib.Data.DFinsupp.Defs
Cited by: 1 results in Mathlib
Foundations: Depth 22 from the axioms · uses propext, Quot.sound
Assumes: Zero DecidableEq

Mathlib docs Source Loogle LeanSearch

Around this declaration

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

Cites2

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

DFinsuppstatement · cited by 694
DFinsupp.singlestatement and proof · cited by 113

Cited by1

Results whose statement or proof uses this declaration.

DirectSum.of_eq_of_gradedMonoid_eqproof · cited by 8