Commit 2025-01-25 11:53 efeadfb1

View on Github →

feat(Data/Matroid/Constructions): Instances for basic matroids (#20886) We add some instances for the matroids in Data/Matroid/Constructions, and also a RkPos -> Nonempty instance in Matroid.Basic.

Estimated changes

Modified Mathlib/Data/Matroid/Basic.lean

Modified Mathlib/Data/Matroid/Constructions.lean

added theorem Matroid.freeOn_rkPos

added theorem Matroid.uniqueBaseOn_finiteRk

added theorem Matroid.uniqueBaseOn_rkPos