Exact incoming sums under finite relabelling #
theorem
MagnitudeConjecture.incoming_sum_eq_of_equiv
{α : Type u}
{β : Type v}
[Fintype α]
[Fintype β]
(e : α ≃ β)
(f : α → α → ℕ)
(g : β → β → ℕ)
(h : ∀ (a b : α), f a b = g (e a) (e b))
(b : α)
:
∑ a : α, f a b = ∑ a : β, g a (e b)