mathlib3

8360f2c8 - feat(model_theory/language_map, bundled): Reducts of structures (#13745)

feat(model_theory/language_map, bundled): Reducts of structures (#13745) Defines `first_order.language.Lhom.reduct` which pulls a structure back along a language map. Defines `first_order.language.Theory.Model.reduct` which sends a model of `(φ.on_Theory T)` to its reduct as a model of `T`.