rw [isIso_emptyOn_iff]
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
α₁ : Type u_4
α₂ : Type u_5
α₃ : Type u_6
M✝ : Matroid α✝
N✝ : Matroid β✝
B I D X Y : Set α✝
M : Matroid α✝
N : Matroid β✝
α : Type u_7
β : Type u_8
⊢ emptyOn α ≂ emptyOn β
no goals