Theorem: Matroid.Simple.loopless (Matroid/Simple.lean)

State before:
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
hM : M.Simple
⊢ M.Loopless
Tactic:
infer_instance
State after:
no goals