Def FirstOrder.Language.ElementaryEmbedding.toHom

Modification history

2023-05-13 13:53

Mathlib/ModelTheory/ElementaryMaps.lean

feat: port ModelTheory.ElementaryMaps (#3931)

Added FirstOrder.Language.ElementaryEmbedding.toHom View on Github →