mathlib

39406bb9 - feat(model_theory/basic): First-order languages, structures, homomorphisms, embeddings, and equivs (#7754)

feat(model_theory/basic): First-order languages, structures, homomorphisms, embeddings, and equivs (#7754) Defines the following notions from first-order logic: - languages - structures - homomorphisms - embeddings - equivalences (isomorphisms) The definitions of languages and structures take inspiration from the Flypitch project.