Theorems · Theorem · general algebraic systems

Finsupp.comapDomain_zero

∀ {α : Type u_1} {β : Type u_2} {M : Type u_5} [inst : Zero M] (f : α → β)
  (hif : optParam (Set.InjOn f (f ⁻¹' ↑(Finsupp.support 0))) ⋯), Finsupp.comapDomain f 0 hif = 0

Note the hif argument is needed for this to work in rw.

Defined in

Mathlib.Data.Finsupp.Basic

Cited by

5 results in Mathlib

Foundations

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

Assumes

Zero