Commit 2025-01-28 03:55 6ac68693

View on Github →

feat(Data/Matroid/Circuit): fundamental circuits and extensionality (#21145) We define the fundamental circuit in a matroid for a set I and an element e, then use it to show that dependent sets all contain circuits, and a circuit-based extensionality lemma.

Estimated changes

Modified Mathlib/Data/Matroid/Circuit.lean

added theorem Matroid.Base.fundCircuit_circuit

modified theorem Matroid.Circuit.circuit_restrict_of_subset

added theorem Matroid.Circuit.eq_fundCircuit_of_subset

added theorem Matroid.Circuit.eq_of_superset_circuit

added theorem Matroid.Dep.exists_circuit_subset

added theorem Matroid.Indep.fundCircuit_circuit

added theorem Matroid.Indep.mem_fundCircuit_iff

added theorem Matroid.dep_iff_superset_circuit'

added theorem Matroid.dep_iff_superset_circuit

added theorem Matroid.ext_circuit

added theorem Matroid.ext_circuit_not_indep

added theorem Matroid.ext_iff_circuit

added def Matroid.fundCircuit

added theorem Matroid.fundCircuit_eq_of_mem'

added theorem Matroid.fundCircuit_eq_of_mem

added theorem Matroid.fundCircuit_eq_sInter

added theorem Matroid.fundCircuit_subset_ground

added theorem Matroid.fundCircuit_subset_insert

added theorem Matroid.indep_iff_forall_subset_not_circuit'

added theorem Matroid.indep_iff_forall_subset_not_circuit

added theorem Matroid.mem_fundCircuit