mathlib

51d81675 - feat(model_theory/elementary_maps): The elementary diagram of a structure (#13724)

feat(model_theory/elementary_maps): The elementary diagram of a structure (#13724) Defines the elementary diagram of a structure - the theory consisting of all sentences with parameters it satisfies. Defines the canonical elementary embedding of a structure into any model of its elementary diagram.