Theorem: Matroid.emptyOn_isIso_iff (Matroid/Old/_Equiv.lean)

State before:
α : 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 β✝
M : Matroid α
β : Type u_7
⊢ emptyOn β ≂ M ↔ M = emptyOn α
Tactic:
rw [IsIso.comm, isIso_emptyOn_iff]
State after:
no goals