Comparing finite sums after removing one index #
Two functions on a finite type that agree away from one index and have the same sum agree everywhere. The result applies to any additive cancellative commutative monoid.
Main results #
TauCeti.eq_of_sum_eq_of_forall_ne: equality of functions from equality of their sums and equality away from one index.
theorem
TauCeti.eq_of_sum_eq_of_forall_ne
{ι : Type u_1}
{M : Type u_2}
[Fintype ι]
[AddCancelCommMonoid M]
(x y : ι → M)
(hsum : ∑ R : ι, x R = ∑ R : ι, y R)
(P : ι)
(h : ∀ (R : ι), R ≠ P → x R = y R)
:
Two functions with equal sums that agree away from one index are equal.