Commit 2024-09-16 17:23 fc1c0e88

feat(ModelTheory/Order): The theory of dense linear orders is countably categorical, and thus complete (#16804) FirstOrder.Language.aleph0_categorical_dlo shows that the theory of dense linear orders is ℵ₀-categorical, as a consequence of Fraïssé theory. As a consequence, it is complete. To aid in calculations (such as needed for deducing completeness) involving the cardinality of a theory, FirstOrder.Language.Symbols is made into an abbrev.