From be2f73b5407793f375c264e716add2b933628a42 Mon Sep 17 00:00:00 2001 From: Eric Date: Thu, 7 Nov 2024 23:36:16 -0800 Subject: [PATCH] Prove that if the positive cone is normal, the group is right ordered --- OrderedSemigroups/OrderedGroup/Basic.lean | 18 +++++++++++++++++- 1 file changed, 17 insertions(+), 1 deletion(-) diff --git a/OrderedSemigroups/OrderedGroup/Basic.lean b/OrderedSemigroups/OrderedGroup/Basic.lean index d6810ca..fc12d70 100644 --- a/OrderedSemigroups/OrderedGroup/Basic.lean +++ b/OrderedSemigroups/OrderedGroup/Basic.lean @@ -138,7 +138,23 @@ def normal_semigroup {α : Type u} [Group α] (x : Subsemigroup α) := A left ordered group whose positive cone is a normal semigroup is an ordered group. -/ def pos_normal_ordered (pos_normal : normal_semigroup (PositiveCone α)) : - ∀ a b : α, a ≤ b → ∀ c : α, a * c ≤ b * c := by sorry + ∀ a b : α, a ≤ b → ∀ c : α, a * c ≤ b * c := by + intro a b a_le_b c + simp [normal_semigroup, PositiveCone] at pos_normal + have : 1 ≤ a⁻¹ * b := le_inv_mul_iff_le.mpr a_le_b + rcases this.eq_or_lt with ainv_b_eq_one | ainv_b_pos + -- Case `a = b` + · have : a*1 = a*(a⁻¹*b) := congrArg (HMul.hMul a) ainv_b_eq_one + simp at this + simp [this] + -- Case `a < b` + have := pos_normal (a⁻¹ * b) ainv_b_pos c⁻¹ + simp at this + have : c * 1 < c * (c⁻¹ * (a⁻¹ * b) * c) := mul_lt_mul_left' this c + simp [mul_one, ←mul_assoc] at this + have : a * c < a * (a⁻¹ * b * c) := mul_lt_mul_left' this a + simp [←mul_assoc] at this + exact this.le end LeftOrdered