Commit 2024-06-07 19:37 77aac96b

View on Github →

feat(Data/Matroid/Constructions): simple constructions of matroids (#12415) The file in this PR constructs all possible matroids that have only one base (these are trivial to describe), and gives some API.

Estimated changes

added def Matroid.emptyOn
added theorem Matroid.emptyOn_ground
added theorem Matroid.empty_base_iff
added theorem Matroid.eq_emptyOn
added theorem Matroid.eq_freeOn_iff
added theorem Matroid.eq_loopyOn_iff
added def Matroid.freeOn
added theorem Matroid.freeOn_dual_eq
added theorem Matroid.freeOn_empty
added theorem Matroid.freeOn_ground
added theorem Matroid.freeOn_indep
added def Matroid.loopyOn
added theorem Matroid.loopyOn_empty
added theorem Matroid.loopyOn_ground
added theorem Matroid.not_rkPos_iff
added theorem Matroid.restrict_empty