Theorem Matroid.IsBasis.isBasis_insert_diff_of_mem_closure

Modification history

2026-06-09 08:51
Mathlib/Combinatorics/Matroid/Closure.lean
chore: rename `diff` to `sdiff` (#40184) …
Deleted Matroid.IsBasis.isBasis_insert_diff_of_mem_closureView on Github →
2025-11-05 19:05
Mathlib/Combinatorics/Matroid/Closure.lean
feat(Matroid): exchange lemmas involving closure (#26510)
Added Matroid.IsBasis.isBasis_insert_diff_of_mem_closureView on Github →