Commit 2025-04-11 12:31 1a3c7400

View on Github →

feat(Matroid): definition of minor (#23873) This PR shows that matroid deletion and contraction commute subject to various disjointness assumptions, and defines the partial order IsMinor on the type Matroid α.

Estimated changes

deleted theorem Matroid.Indep.of_delete
deleted theorem Matroid.IsBasis.delete
deleted theorem Matroid.IsBasis.of_delete
deleted def Matroid.delete
deleted theorem Matroid.delete_closure_eq
deleted theorem Matroid.delete_comm
deleted theorem Matroid.delete_compl
deleted theorem Matroid.delete_delete
deleted theorem Matroid.delete_dep_iff
deleted theorem Matroid.delete_empty
deleted theorem Matroid.delete_ground
deleted theorem Matroid.delete_indep_iff
deleted theorem Matroid.delete_isBase_iff
deleted theorem Matroid.delete_isLoop_iff
deleted theorem Matroid.delete_loops_eq
deleted theorem Matroid.restrict_compl
added theorem Matroid.IsBasis.delete
added def Matroid.delete
added theorem Matroid.delete_comm
added theorem Matroid.delete_compl
added theorem Matroid.delete_delete
added theorem Matroid.delete_dep_iff
added theorem Matroid.delete_empty
added theorem Matroid.delete_ground
added theorem Matroid.restrict_compl
added theorem Matroid.Dep.of_isMinor
added theorem Matroid.IsMinor.le
added theorem Matroid.IsMinor.refl
added theorem Matroid.IsMinor.subset
added theorem Matroid.IsMinor.trans
added def Matroid.IsMinor
added theorem Matroid.le_eq_isMinor