Commit 2021-09-17 12:18 5f140ab4

View on Github →

chore(*): rename coe_fn_inj to coe_fn_injective (#9241) This also removes some comments about it not being possible to use function.injective, since now we use it without problem.

Estimated changes

Modified src/algebra/algebra/basic.lean

deleted theorem alg_hom.coe_fn_inj

added theorem alg_hom.coe_fn_injective

Modified src/algebra/category/Algebra/limits.lean

Modified src/linear_algebra/affine_space/affine_equiv.lean

modified theorem affine_equiv.coe_fn_injective

Modified src/order/rel_iso.lean

deleted theorem rel_embedding.coe_fn_inj

added theorem rel_embedding.coe_fn_injective

deleted theorem rel_hom.coe_fn_inj

added theorem rel_hom.coe_fn_injective

Modified src/set_theory/ordinal.lean