Theorems · Theorem · general algebraic systems

DFinsupp.neLocus_add_left

∀ {α : Type u_1} {N : α → Type u_2} [inst : DecidableEq α] [inst_1 : (a : α) → DecidableEq (N a)]
  [inst_2 : (a : α) → AddLeftCancelMonoid (N a)] (f g h : Π₀ (a : α), N a), (f + g).neLocus (f + h) = g.neLocus h

Defined in

Mathlib.Data.DFinsupp.NeLocus

Cited by

2 results in Mathlib

Foundations

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

Assumes

DecidableEqDecidableEqAddLeftCancelMonoid