unfold mpDsum
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M N : MultiPart α
hA : M.A = N.A
ht : M.t = N.t
iM : TuranPartition M
iN : TuranPartition N
⊢ mpDsum M = mpDsum N
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M N : MultiPart α
hA : M.A = N.A
ht : M.t = N.t
iM : TuranPartition M
iN : TuranPartition N
⊢ ∑ v in M.A, degree (mp M) v = ∑ v in N.A, degree (mp N) v