Theorem: Matroid.ModularCut.extension_indep (Matroid/Old/_ModularCut.lean)

State before:
α : Type u_1
M : Matroid α
I✝ B : Set α
Ys Xs : Set (Set α)
C : M.ModularCut
e : α
I : Set α
⊢ (C.extension e).Indep I ↔ M.Indep I ∨ e ∈ I \ M.E ∧ M.Indep (I \ {e}) ∧ M.cl (I \ {e}) ∉ C
Tactic:
simp [extension]
State after:
no goals