Theorems · Theorem · general algebraic systems

DFinsupp.comapDomain_single

∀ {ι : Type u} {β : ι → Type v} {κ : Type u_1} [inst : DecidableEq ι] [inst_1 : DecidableEq κ]
  [inst_2 : (i : ι) → Zero (β i)] (h : κ → ι) (hh : Function.Injective h) (k : κ) (x : β (h k)),
  (DFinsupp.comapDomain h hh fun₀ | h k => x) = fun₀ | k => x

Defined in

Mathlib.Data.DFinsupp.Defs

Cited by

0 results in Mathlib

Foundations

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

Assumes

DecidableEqDecidableEqZero