English
For any index i and elements a,b in α, we have the equality single i (a - b) = single i a - single i b, where - on the right is truncated subtraction in α.
Русский
Для любого индекса i и элементов a,b из α выполняется равенство single i (a - b) = single i a - single i b, где - на правой стороне означает усечение вычитания в α.
LaTeX
$$$\\mathrm{single}(i, (a - b)) = \\mathrm{single}(i, a) - \\mathrm{single}(i, b)$$$
Lean4
@[simp]
theorem single_tsub : single i (a - b) = single i a - single i b :=
by
ext j
obtain rfl | h := eq_or_ne j i
· rw [tsub_apply, single_eq_same, single_eq_same, single_eq_same]
· rw [tsub_apply, single_eq_of_ne h, single_eq_of_ne h, single_eq_of_ne h, tsub_self]
