English
There is a truncated subtraction on finsupps: for any f,g : ι →₀ α, the operation f - g is defined pointwise by (f - g)(i) = f(i) - g(i) (with truncation to 0 in the canonically ordered setting).
Русский
Существуют усечение вычитания на FinSupp: для любых f,g : ι →₀ α определение (f - g)(i) равно f(i) - g(i) с ограничением снизу 0 в канонически упорядоченном наборе.
LaTeX
$$$ (f - g)(i) = f(i) - g(i) \\quad \\text{для всех } i$$$
Lean4
/-- This is called `tsub` for truncated subtraction, to distinguish it with subtraction in an
additive group. -/
instance tsub : Sub (ι →₀ α) :=
⟨zipWith (fun m n => m - n) (tsub_self 0)⟩
