mathlib3

9ce5e95a - feat(model_theory/syntax, semantics): A theory of infinite structures (#13580)

feat(model_theory/syntax, semantics): A theory of infinite structures (#13580) Defines `first_order.language.infinite_theory`, a theory of infinite structures Adjusts the API of the theory of nonempty structures to match