Commit 2025-01-25 16:29 01b13023

View on Github →

feat(Data/Matroid/Circuit): Matroid circuits (#20995) We define and give basis API for circuits (minimal dependent sets) in matroids.

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/Matroid/Circuit.lean

added theorem Matroid.Circuit.basis_iff_eq_diff_singleton

added theorem Matroid.Circuit.basis_iff_insert_eq

added theorem Matroid.Circuit.circuit_restrict_of_subset

added theorem Matroid.Circuit.closure_diff_singleton_eq

added theorem Matroid.Circuit.dep

added theorem Matroid.Circuit.diff_singleton_basis

added theorem Matroid.Circuit.diff_singleton_indep

added theorem Matroid.Circuit.eq_of_dep_subset

added theorem Matroid.Circuit.eq_of_not_indep_subset

added theorem Matroid.Circuit.eq_of_subset_circuit

added theorem Matroid.Circuit.mem_closure_diff_singleton_of_mem

added theorem Matroid.Circuit.minimal

added theorem Matroid.Circuit.minimal_not_indep

added theorem Matroid.Circuit.nonempty

added theorem Matroid.Circuit.not_indep

added theorem Matroid.Circuit.not_ssubset

added theorem Matroid.Circuit.ssubset_indep

added theorem Matroid.Circuit.subset_closure_diff_singleton

added theorem Matroid.Circuit.subset_ground

added def Matroid.Circuit

added theorem Matroid.Indep.insert_circuit_of_forall

added theorem Matroid.Indep.insert_circuit_of_forall_of_nontrivial

added theorem Matroid.circuit_antichain

added theorem Matroid.circuit_def

added theorem Matroid.circuit_iff

added theorem Matroid.circuit_iff_dep_forall_diff_singleton_indep

added theorem Matroid.circuit_iff_forall_ssubset

added theorem Matroid.circuit_iff_minimal_not_indep

added theorem Matroid.empty_not_circuit

added theorem Matroid.restrict_circuit_iff