English
In a cancellative additive commutative monoid, a linear combination of two singleton functions is unique up to the listed symmetries: (k,l) = (m,n), or (u=v and k=n and l=m), or (u+v=0 and k=l and m=n).
Русский
В дополнительно отменяемом аддитивном коммутативном моноиде представление суммы двух сигмальных функций уникально: (k,l)=(m,n) либо (u=v и k=n и l=m) либо (u+v=0 и k=l и m=n).
LaTeX
$$$\forall k,l,m,n:\ ι,\forall u,v:\ M\,(hu: u \neq 0) (hv: v \neq 0) :\
(\text{single } k u + \text{single } l v = \text{single } m u + \text{single } n v) \\iff ((k=m \wedge l=n) \lor (u=v \wedge k=n \wedge l=m) \lor (u+v=0 \wedge k=l \wedge m=n))$$$
Lean4
theorem single_add_single_eq_single_add_single {k l m n : ι} {u v : M} (hu : u ≠ 0) (hv : v ≠ 0) :
single k u + single l v = single m u + single n v ↔
(k = m ∧ l = n) ∨ (u = v ∧ k = n ∧ l = m) ∨ (u + v = 0 ∧ k = l ∧ m = n) :=
by
classical
simp_rw [DFunLike.ext_iff, coe_add, single_eq_pi_single, ← funext_iff]
exact Pi.single_add_single_eq_single_add_single hu hv
