exact mp_deg ⟨hx, hv⟩
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
x : ℕ
hx : x ∈ range (M.t + 1)
v : α
hv : v ∈ MultiPart.P M x
⊢ degree (mp M) v = card (M.A \ MultiPart.P M x)
no goals