feat(Data/Matroid/Circuit): Matroid circuits

[apnelson1]

We define and give basis API for circuits (minimal dependent sets) in matroids.

---

[github-actions]

PR summary 9827e093c1

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
Mathlib.Data.Matroid.Circuit (new file)	704

---

Declarations diff

+ Circuit
+ Circuit.basis_iff_eq_diff_singleton
+ Circuit.basis_iff_insert_eq
+ Circuit.circuit_restrict_of_subset
+ Circuit.closure_diff_singleton_eq
+ Circuit.closure_diff_subsingleton_eq
+ Circuit.dep
+ Circuit.diff_singleton_basis
+ Circuit.diff_singleton_indep
+ Circuit.eq_of_dep_subset
+ Circuit.eq_of_not_indep_subset
+ Circuit.eq_of_subset_circuit
+ Circuit.mem_closure_diff_singleton_of_mem
+ Circuit.minimal
+ Circuit.nonempty
+ Circuit.not_indep
+ Circuit.not_ssubset
+ Circuit.ssubset_indep
+ Circuit.subset_closure_diff_singleton
+ Circuit.subset_closure_diff_subsingleton
+ Circuit.subset_ground
+ Indep.insert_circuit_of_forall
+ Indep.insert_circuit_of_forall_of_nontrivial
+ circuit_antichain
+ circuit_def
+ circuit_iff
+ circuit_iff_dep_forall_diff_singleton_indep
+ circuit_iff_forall_ssubset
+ empty_not_circuit
+ restrict_circuit_iff

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

---

No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[AntoineChambert-Loir]

Is this already formalized?

[apnelson1]

Yes, but currently just in my repo. It should be part of the next PR, so I thought that including the comment made sense as some general motivation for the notion of a circuit.

[apnelson1]

(I'm assuming by 'this' you are referring to the implied extensionality statement)