mathlib

114f5436 - feat(model_theory/semantics, elementary_maps): Defines elementary equivalence (#14723)

feat(model_theory/semantics, elementary_maps): Defines elementary equivalence (#14723) Defines elementary equivalence of structures Shows that the domain and codomain of an elementary map are elementarily equivalent.