Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-05-09 14:40 31af0e88

View on Github →

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 κ.

Estimated changes