mathlib3

15444e1f - feat(model_theory/basic): more substructure API, including subtype, map, and comap (#7937)

feat(model_theory/basic): more substructure API, including subtype, map, and comap (#7937) Defines `first_order.language.embedding.of_injective`, which bundles an injective hom in an algebraic language as an embedding Defines the induced `L.Structure` on an `L.substructure` Defines the embedding `S.subtype` from `S : L.substructure M` into `M` Defines `substructure.map` and `substructure.comap` and associated API including Galois insertions