mathlib3

8050ac7c - feat(set_theory/zfc/basic): `inj` lemmas (#15545)

feat(set_theory/zfc/basic): `inj` lemmas (#15545) We rename two existing lemmas from `*_inj` to `*_injective` to match mathlib convention, and add the corresponding `inj` lemmas.