Commit 2025-11-05 19:05 6b973c33

View on Github →

feat(Matroid): exchange lemmas involving closure (#26510)

Estimated changes

Modified Mathlib/Combinatorics/Matroid/Closure.lean

added theorem Matroid.Indep.closure_insert_diff_eq_of_mem_closure

added theorem Matroid.Indep.indep_insert_diff_of_mem_closure

added theorem Matroid.IsBase.isBase_insert_diff_of_mem_closure

added theorem Matroid.IsBasis.isBasis_insert_diff_of_mem_closure