theorem Matroid.disjointSum_comm {α : Type u_1} {M : Matroid α} {N : Matroid α} (hMN : Disjoint M.E N.E) : M.disjointSum N hMN = N.disjointSum M ⋯