Commit 2025-01-20 15:06 30811210

View on Github →

chore(Data/Matroid/Basic): a few tweaks to Matroid.Basic (#19836) We make a few small QOL changes to Matroid.Basic:

  • added @[mk_iff] to a few typeclass defs, in one case replacing the manually defined lemma with the automatic one in the places it's later used.
  • added a lemma about base exchanges
  • added a lemma proving that a Nonempty matroid lives in a Nonempty type.

Estimated changes

added theorem Matroid.nonempty_type