mathlib

31af0e88 - feat(model_theory/satisfiability): Definition of categorical theories (#14038)

feat(model_theory/satisfiability): Definition of categorical theories (#14038) Defines that a first-order theory is `κ`-categorical when all models of cardinality `κ` are isomorphic. Shows that all theories in the empty language are `κ`-categorical for all cardinals `κ`.