Def FirstOrder.Language.Embedding.toElementaryEmbedding

Modification history

2023-05-13 13:53

Mathlib/ModelTheory/ElementaryMaps.lean

feat: port ModelTheory.ElementaryMaps (#3931)

Added FirstOrder.Language.Embedding.toElementaryEmbedding View on Github →