mathlib3
31391dc2 - feat(model_theory/basic, elementary_maps): Uses `fun_like` approach for first-order maps (#12755)

Commit

3 years ago

feat(model_theory/basic, elementary_maps): Uses `fun_like` approach for first-order maps (#12755) Introduces classes `hom_class`, `strong_hom_class` to describe classes of first-order maps.

Author

awainverse

Parents

9d7a6645

mathlib3 31391dc2 - feat(model_theory/basic, elementary_maps): Uses `fun_like` approach for first-order maps (#12755)

mathlib3
31391dc2 - feat(model_theory/basic, elementary_maps): Uses `fun_like` approach for first-order maps (#12755)