Commit 2024-07-31 06:03 0c8f6eb2
View on Github →chore(ModelTheory/Complexity): move quantifier complexity into a new file (#15275)
Several important files in the model theory library touch on quantifier complexity of formulas, an idea that is not yet used for anything else in mathlib
.
This PR moves all quantifier complexity content to a new file, ModelTheory/Complexity
and improves the documentation of these concepts.
This will hopefully make these basic files more legible and easier to refactor.