Theorem: Matroid.empty_basis_iff (Matroid/Closure.lean)

State before:
α : Type u_1
ι : Type u_2
M : Matroid α
F I J X Y B C R : Set α
e f x y : α
⊢ M.Basis ∅ X ↔ X ⊆ M.cl ∅
Tactic:
rw [basis_iff_indep_cl, and_iff_right M.empty_indep, and_iff_left (empty_subset _)]
State after:
no goals