Commit 2025-01-20 16:09 82838c6a

feat(Data/Matroid/IndepAxioms): Another constructor for finitary matroids (#20877) This PR adds a new constructor for a finitary matroid, via IndepMatroid. The constructor uses the infinite independence augmentation axiom, together with a compactness assumption for independence. We name it IndepMatroid.ofFinitary, and rename the already existing variant with that name IndepMatroid.ofFinitaryCardAugment, since the former is really more canonical. This was motivated by the application of algebraic matroids to transcendence degrees, as discussed on zulip