Theorems · Theorem · general algebraic systems

DFinsupp.mapRange_neLocus_eq

∀ {α : Type u_1} {N : α → Type u_2} [inst : DecidableEq α] {M : α → Type u_3} [inst_1 : (a : α) → Zero (N a)]
  [inst_2 : (a : α) → Zero (M a)] [inst_3 : (a : α) → DecidableEq (N a)] [inst_4 : (a : α) → DecidableEq (M a)]
  (f g : Π₀ (a : α), N a) {F : (a : α) → N a → M a} (F0 : ∀ (a : α), F a 0 = 0),
  (∀ (a : α), Function.Injective (F a)) → (DFinsupp.mapRange F F0 f).neLocus (DFinsupp.mapRange F F0 g) = f.neLocus g

Defined in

Mathlib.Data.DFinsupp.NeLocus

Cited by

1 results in Mathlib

Foundations

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

Assumes

DecidableEqZeroZeroDecidableEqDecidableEq