Commit 2022-12-14 15:48 ef428bf9

View on Github →

feat port: Algebra.Order.Field.InjSurj (#1017) ee0c179cd3c8a45aa5bffbf1b41d8dbede452865

Estimated changes

Modified Mathlib.lean

Created Mathlib/Algebra/Order/Field/InjSurj.lean

added def Function.Injective.linearOrderedField

added def Function.Injective.linearOrderedSemifield