Mathlib v3 is deprecated. Go to Mathlib v4

Def nonneg_comm_group.to_decidable_linear_ordered_comm_group

Modification history

2020-04-11 04:27
src/algebra/ordered_group.lean
chore(*): switch to lean 3.8.0 (#2361) …
Deleted nonneg_comm_group.to_decidable_linear_ordered_comm_groupView on Github →
2017-09-16 02:53
algebra/ordered_group.lean
feat(algebra): new algebra theorems (more iff)
Added nonneg_comm_group.to_decidable_linear_ordered_comm_groupView on Github →