Theorems · Definition · general algebraic systems

DFinsupp.filterAddMonoidHom

{ι : Type u} →
  (β : ι → Type v) →
    [inst : (i : ι) → AddZeroClass (β i)] → (p : ι → Prop) → [DecidablePred p] → (Π₀ (i : ι), β i) →+ Π₀ (i : ι), β i

DFinsupp.filter as an AddMonoidHom.

Defined in: Mathlib.Data.DFinsupp.Defs
Cited by: 5 results in Mathlib
Foundations: Depth 27 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: AddZeroClass DecidablePred

Mathlib docs Source Loogle LeanSearch

Around this declaration

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

Cites5

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

AddMonoidHomstatement · cited by 3,230
AddZeroClassstatement and proof · cited by 1,237
DFinsuppstatement · cited by 694
DFinsupp.filterproof · cited by 24
DFinsupp.filter_addproof · cited by 0

Cited by5

Results whose statement or proof uses this declaration.

AddSubmonoid.bsupr_eq_mrange_dfinsuppSumAddHomstatement and proof · cited by 1
DFinsupp.filterAddMonoidHom_applystatement and proof · cited by 1
DFinsupp.filterAddMonoidHom.congr_simpstatement and proof · cited by 0
DFinsupp.filter_negproof · cited by 0
DFinsupp.filter_subproof · cited by 0