mathlib3
e326fe60 - feat(model_theory/basic,language_map): More about `language.mk₂` (#13090)

Commit
3 years ago
feat(model_theory/basic,language_map): More about `language.mk₂` (#13090) Provides instances on `language.mk₂` Defines `first_order.language.Lhom.mk₂`, a constructor for maps from languages built with `language.mk₂`.
Author
Parents
Loading