ordered_comm_group

Stream: general

[Reid Barton]

ordered_comm_group is defined in core and it has two fields:

class ordered_comm_group (α : Type u) extends add_comm_group α, partial_order α :=
(add_le_add_left : ∀ a b : α, a ≤ b → ∀ c : α, c + a ≤ c + b)
(add_lt_add_left : ∀ a b : α, a < b → ∀ c : α, c + a < c + b)

Am I really confused or does the second one follow from the first? If c + a >= c + b, then add -c to both sides.

[Reid Barton]

In fact it looks like this was already noticed for ordered_cancel_comm_monoid

[Floris van Doorn]

Yeah, that's right (it's actually the first lemma below the definition). But it's in core...

[Chris Hughes]

There are tons of unneceassary axioms in core. field for example asks for proof of left inverses and right inverse.

[Reid Barton]

Is that because it extends division_ring or something?

[Chris Hughes]

Yes.