Commit 2023-10-30 21:12 aaa97c71

feat: (Data.Matroid) basic matroid theory (#6352) This PR is the first in a series that are intended to add matroid theory to mathlib. The file Data.Matroid.Basic contains the definition of (possibly infinite) matroids, API relating bases, independent/dependent sets and bases of sets, and some simple typeclasses related to finiteness/nonemptiness of matroids. We also define a tactic whose job is to prove that a set is contained in the ground set of a matroid (using aesop); it is imperfect, but does an ok job.

Alternative axiomatizations, duality, minors, rank, circuits, closure, flats, etc etc are all ready to go, and will be added in a sequence of future PRs.