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

Commit

4 years ago

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.

Author

eric-wieser

Parents

3309ce27

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

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