Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-03-17 09:56 31391dc2

View on Github →

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.

Estimated changes

Modified src/model_theory/basic.lean

modified structure first_order.language.embedding

added theorem first_order.language.equiv.bijective

modified theorem first_order.language.equiv.coe_injective

modified theorem first_order.language.equiv.injective

added theorem first_order.language.equiv.surjective

deleted theorem first_order.language.hom.coe_injective

added theorem first_order.language.hom_class.map_constants

added def first_order.language.hom_class.strong_hom_class_of_is_algebraic

Modified src/model_theory/elementary_maps.lean

modified theorem first_order.language.elementary_embedding.coe_injective