Commit 2022-12-14 09:49 d11e0f3d

View on Github →

feat: port Algebra.Order.Invertible (#1006) ee0c179cd3c8a45aa5bffbf1b41d8dbede452865

Estimated changes

Modified Mathlib.lean

Created Mathlib/Algebra/Order/Invertible.lean

added theorem invOf_le_one

added theorem invOf_lt_zero

added theorem invOf_nonneg

added theorem invOf_nonpos

added theorem invOf_pos