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.

Estimated changes