Theorems · Theorem · general algebraic systems

Finsupp.subtypeDomain_eq_iff

∀ {α : Type u_1} {M : Type u_5} [inst : Zero M] {p : α → Prop} {f g : α →₀ M},
  (∀ x ∈ f.support, p x) → (∀ x ∈ g.support, p x) → (Finsupp.subtypeDomain p f = Finsupp.subtypeDomain p g ↔ f = g)

Defined in

Mathlib.Data.Finsupp.Basic

Cited by

2 results in Mathlib

Foundations

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

Assumes

Zero