lean4-htt/library/init/algebra
Mario Carneiro 0f7fdae33e refactor(algebra/ordered_group): remove redundant axioms
for ordered_cancel_comm_monoid. The change to partial_order, with a derived lt relation, makes the lt axioms of ordered groups derivable with no additional assumptions.
2017-10-23 12:20:42 -07:00
..
classes.lean feat(library/class): add attribute for tracking symbols occurring in instances of type classes 2017-05-01 18:02:30 -07:00
default.lean feat(library/init/algebra): add discrete_linear_ordered_field 2016-12-17 21:18:59 -08:00
field.lean feat(library/init/meta/interactive): rw [-h] ==> rw [← h] 2017-07-05 11:42:55 -07:00
functions.lean refactor(library/init/algebra): remove order_pair classes 2017-08-02 14:41:35 +01:00
group.lean chore(init/algebra/group): generalize to noncomm groups 2017-09-15 12:33:46 -07:00
norm_num.lean feat(library/init/meta/interactive): rw [-h] ==> rw [← h] 2017-07-05 11:42:55 -07:00
order.lean chore(library/init/algebra/order): generalize lemma 2017-08-06 09:58:24 +02:00
ordered_field.lean fix(library/init/algebra/ordered_field): remove unused argument from div_two_lt_of_pos 2017-08-24 16:27:42 +02:00
ordered_group.lean refactor(algebra/ordered_group): remove redundant axioms 2017-10-23 12:20:42 -07:00
ordered_ring.lean refactor(algebra/ordered_group): remove redundant axioms 2017-10-23 12:20:42 -07:00
ring.lean feat(library/init/meta/interactive): rw [-h] ==> rw [← h] 2017-07-05 11:42:55 -07:00