Reid Barton (Aug 21 2019 at 15:11):
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 (Aug 21 2019 at 15:13):
In fact it looks like this was already noticed for
Floris van Doorn (Aug 21 2019 at 15:33):
Yeah, that's right (it's actually the first lemma below the definition). But it's in core...
Chris Hughes (Aug 21 2019 at 15:35):
There are tons of unneceassary axioms in core.
field for example asks for proof of left inverses and right inverse.
Reid Barton (Aug 21 2019 at 15:37):
Is that because it extends
division_ring or something?
Chris Hughes (Aug 21 2019 at 15:39):
Last updated: Aug 03 2023 at 10:10 UTC