Theorems · Theorem · order theory

DFinsupp.single_tsub

∀ {ι : Type u_1} {α : ι → Type u_2} [inst : (i : ι) → AddCommMonoid (α i)] [inst_1 : (i : ι) → PartialOrder (α i)]
  [inst_2 : ∀ (i : ι), CanonicallyOrderedAdd (α i)] [inst_3 : (i : ι) → Sub (α i)]
  [inst_4 : ∀ (i : ι), OrderedSub (α i)] {i : ι} {a b : α i} [inst_5 : DecidableEq ι],
  (fun₀ | i => a - b) = (fun₀ | i => a) - fun₀ | i => b

Defined in

Mathlib.Data.DFinsupp.Order

Cited by

0 results in Mathlib

Foundations

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

Assumes

AddCommMonoidPartialOrderCanonicallyOrderedAddSubOrderedSubDecidableEq