Commit 2025-01-30 00:58 0cd97635

feat(Data/Matroid/Circuit): better junk values for fundCircuit (#21240) The definition of fundamental circuits in #21145 was suboptimal, in that its junk values were unstable. We slightly modify the definition so that the fundamental circuit of a non-element e of the ground set is a singleton {e}. This removes assumptions from a couple of existing lemmas, and crucially makes the useful lemma Matroid.fundCircuit_restrict_univ true, where it wasn't before.