mathlib

ff507a35 - feat(model_theory/basic): Structures over the empty language (#13281)

feat(model_theory/basic): Structures over the empty language (#13281) Any type is a first-order structure over the empty language. Any function, embedding, or equiv is a first-order hom, embedding or equiv over the empty language.