Commit 2025-02-05 21:25 3ebd28c3

View on Github →

feat(Data/Matroid/Circuit): circuit elimination and finitary matroids (#21172) We add various version of the circuit elimination axiom, and some lemmas about finitary matroids.

Estimated changes

Modified Mathlib/Data/Matroid/Circuit.lean

added theorem Matroid.Circuit.elimination

modified theorem Matroid.Circuit.eq_fundCircuit_of_subset

added theorem Matroid.Circuit.finite

added theorem Matroid.Circuit.strong_elimination

added theorem Matroid.Circuit.strong_multi_elimination

added theorem Matroid.Circuit.strong_multi_elimination_insert

added theorem Matroid.Circuit.strong_multi_elimination_set

added theorem Matroid.exists_circuit_of_mem_closure

added theorem Matroid.exists_mem_finite_closure_of_mem_closure

added theorem Matroid.exists_subset_finite_closure_of_subset_closure

added theorem Matroid.finitary_iff_forall_circuit_finite

added theorem Matroid.mem_closure_iff_exists_circuit