From 00200778d534c631c0196f84eb4cdcb76c35247d Mon Sep 17 00:00:00 2001 From: Kevin Buzzard Date: Wed, 25 Nov 2020 03:17:58 +0000 Subject: [PATCH] fix(algebra/ordered_group): remove workaround (#5103) The problem mentioned in the TODO has been solved so the workaround is no longer needed. --- src/algebra/ordered_group.lean | 18 ------------------ src/set_theory/game.lean | 6 +++--- 2 files changed, 3 insertions(+), 21 deletions(-) diff --git a/src/algebra/ordered_group.lean b/src/algebra/ordered_group.lean index 15dde02fc49e3..11c6da9a71f83 100644 --- a/src/algebra/ordered_group.lean +++ b/src/algebra/ordered_group.lean @@ -682,24 +682,6 @@ sub_lt_iff_lt_add'.trans (lt_add_iff_pos_left _) end ordered_add_comm_group -/- -TODO: -The `add_lt_add_left` field of `ordered_add_comm_group` is redundant, -and it is no longer in core so we can remove it now. -This alternative constructor is a workaround until someone fixes this. --/ - -/-- Alternative constructor for ordered commutative groups, -that avoids the field `mul_lt_mul_left`. -/ -@[to_additive "Alternative constructor for ordered commutative groups, -that avoids the field `mul_lt_mul_left`."] -def ordered_comm_group.mk' {α : Type u} [comm_group α] [partial_order α] - (mul_le_mul_left : ∀ a b : α, a ≤ b → ∀ c : α, c * a ≤ c * b) : - ordered_comm_group α := -{ mul_le_mul_left := mul_le_mul_left, - ..(by apply_instance : comm_group α), - ..(by apply_instance : partial_order α) } - /-- A decidable linearly ordered additive commutative group is an additive commutative group with a decidable linear order in which addition is strictly monotone. -/ diff --git a/src/set_theory/game.lean b/src/set_theory/game.lean index 0eb7c9546187a..33f822ce6f1d8 100644 --- a/src/set_theory/game.lean +++ b/src/set_theory/game.lean @@ -157,10 +157,10 @@ def game_partial_order : partial_order game := le_antisymm := le_antisymm, ..game.has_le } -local attribute [instance] game_partial_order - /-- The `<` operation provided by this `ordered_add_comm_group` is not the usual `<` on games! -/ def ordered_add_comm_group_game : ordered_add_comm_group game := -ordered_add_comm_group.mk' add_le_add_left +{ add_le_add_left := add_le_add_left, + ..game.add_comm_group, + ..game_partial_order } end game