Theorems · Theorem · general algebraic systems

Finsupp.mk.congr_simp

∀ {α : Type u_9} {M : Type u_10} [inst : Zero M] (support support_1 : Finset α) (e_support : support = support_1)
  (toFun toFun_1 : α → M) (e_toFun : toFun = toFun_1) (mem_support_toFun : ∀ (a : α), a ∈ support ↔ toFun a ≠ 0),
  { support := support, toFun := toFun, mem_support_toFun := mem_support_toFun } =
    { support := support_1, toFun := toFun_1, mem_support_toFun := ⋯ }

Defined in

Mathlib.Data.Finsupp.Defs

Cited by

9 results in Mathlib

Foundations

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

Assumes

Zero