Commit 2024-06-07 11:39 42772142

View on Github →

feat(Algebra/Order/GroupWithZero): add inv_lt_one₀ and one_lt_inv₀ (#13563) add inv_lt_one₀ and one_lt_inv₀

Estimated changes

added theorem inv_lt_one₀
added theorem one_lt_inv₀