Magnitude conjecture

MagnitudeConjecture.Combinatorics.ReindexedIncomingEquality

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)