feat(algebra/field): add function.injective.field (#6511)
feat(algebra/field): add function.injective.field (#6511)

We already have defs of this style for all sorts of algebraic constructions, why not one more.





leanprover-community/mathlib,leanprover-community/mathlib