Zulip Chat Archive

Stream: Is there code for X?

Topic: defining matroids by circuits

Lua Viana Reis (Jul 04 2025 at 02:22):

Is there a quicker way to define a finite matroid by a set of circuits satisfying some conditions, other than "manually" via IndepMatroid.ofFinite?

Johan Commelin (Jul 04 2025 at 02:23):

cc @Peter Nelson

Peter Nelson (Jul 04 2025 at 02:32):

Not in mathlib, but in the repo - see FiniteCircuitMatroid.matroid. The file is a bit chicken-scratchy, but everything typechecks.

Lua Viana Reis (Jul 04 2025 at 02:32):

thanks a lot!

Peter Nelson (Jul 04 2025 at 11:28):

Can I ask what matroid you are looking to define?

Lua Viana Reis (Jul 04 2025 at 14:04):

It's the Fano matroid

Last updated: Dec 20 2025 at 21:32 UTC