mathlib

043a74e2 - feat(model_theory/satisfiability): Maximally consistent theories (#16547)

feat(model_theory/satisfiability): Maximally consistent theories (#16547) Defines `first_order.language.Theory.is_maximal` to denote maximally consistent theories Shows that such theories are complete, and that the complete theory of a structure, as constructed, is maximal Co-authored-by: Aaron Anderson <65780815+awainverse@users.noreply.github.com>