diff --git a/Mathlib.lean b/Mathlib.lean index 88571562b0e33..51acd3292ba91 100644 --- a/Mathlib.lean +++ b/Mathlib.lean @@ -375,7 +375,6 @@ import Mathlib.Algebra.Order.Interval import Mathlib.Algebra.Order.Invertible import Mathlib.Algebra.Order.Kleene import Mathlib.Algebra.Order.LatticeGroup -import Mathlib.Algebra.Order.Module import Mathlib.Algebra.Order.Module.Defs import Mathlib.Algebra.Order.Module.OrderedSMul import Mathlib.Algebra.Order.Module.Pointwise diff --git a/Mathlib/Algebra/Order/Module.lean b/Mathlib/Algebra/Order/Module.lean deleted file mode 100644 index 320cba192aadf..0000000000000 --- a/Mathlib/Algebra/Order/Module.lean +++ /dev/null @@ -1,279 +0,0 @@ -/- -Copyright (c) 2020 Frédéric Dupuis. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. -Authors: Frédéric Dupuis, Yaël Dillies --/ -import Mathlib.Algebra.Order.Module.OrderedSMul - -#align_import algebra.order.module from "leanprover-community/mathlib"@"3ba15165bd6927679be7c22d6091a87337e3cd0c" - -/-! -# Ordered module - -In this file we provide lemmas about `OrderedSMul` that hold once a module structure is present. - -## TODO - -Generalise lemmas to the framework from `Mathlib.Algebra.Order.Module.Defs`. - -## References - -* https://en.wikipedia.org/wiki/Ordered_vector_space - -## Tags - -ordered module, ordered scalar, ordered smul, ordered action, ordered vector space --/ - - -open Pointwise - -variable {ι k M N : Type*} - -section Semiring - -variable [OrderedSemiring k] [OrderedAddCommGroup M] [Module k M] [OrderedSMul k M] {a b : M} - {c : k} - -/- Can be generalized from `Module k M` to `DistribMulActionWithZero k M` once it exists. -where `DistribMulActionWithZero k M`is the conjunction of `DistribMulAction k M` and -`SMulWithZero k M`.-/ -theorem smul_neg_iff_of_pos (hc : 0 < c) : c • a < 0 ↔ a < 0 := by - rw [← neg_neg a, smul_neg, neg_neg_iff_pos, neg_neg_iff_pos] - exact smul_pos_iff_of_pos_left hc -#align smul_neg_iff_of_pos smul_neg_iff_of_pos - -end Semiring - -section Ring - -variable [OrderedRing k] [OrderedAddCommGroup M] [Module k M] [OrderedSMul k M] {a b : M} {c d : k} - -theorem smul_lt_smul_of_neg (h : a < b) (hc : c < 0) : c • b < c • a := by - rw [← neg_neg c, neg_smul, neg_smul (-c), neg_lt_neg_iff] - exact smul_lt_smul_of_pos_left h (neg_pos_of_neg hc) -#align smul_lt_smul_of_neg smul_lt_smul_of_neg - -theorem smul_le_smul_of_nonpos (h : a ≤ b) (hc : c ≤ 0) : c • b ≤ c • a := by - rw [← neg_neg c, neg_smul, neg_smul (-c), neg_le_neg_iff] - exact smul_le_smul_of_nonneg_left h (neg_nonneg_of_nonpos hc) -#align smul_le_smul_of_nonpos smul_le_smul_of_nonpos - -#noalign eq_of_smul_eq_smul_of_neg_of_le - -theorem lt_of_smul_lt_smul_of_nonpos (h : c • a < c • b) (hc : c ≤ 0) : b < a := by - rw [← neg_neg c, neg_smul, neg_smul (-c), neg_lt_neg_iff] at h - exact lt_of_smul_lt_smul_of_nonneg_left h (neg_nonneg_of_nonpos hc) -#align lt_of_smul_lt_smul_of_nonpos lt_of_smul_lt_smul_of_nonpos - -theorem smul_lt_smul_iff_of_neg (hc : c < 0) : c • a < c • b ↔ b < a := by - rw [← neg_neg c, neg_smul, neg_smul (-c), neg_lt_neg_iff] - exact smul_lt_smul_iff_of_pos_left (neg_pos_of_neg hc) -#align smul_lt_smul_iff_of_neg smul_lt_smul_iff_of_neg - -theorem smul_neg_iff_of_neg (hc : c < 0) : c • a < 0 ↔ 0 < a := by - rw [← neg_neg c, neg_smul, neg_neg_iff_pos] - exact smul_pos_iff_of_pos_left (neg_pos_of_neg hc) -#align smul_neg_iff_of_neg smul_neg_iff_of_neg - -theorem smul_pos_iff_of_neg (hc : c < 0) : 0 < c • a ↔ a < 0 := by - rw [← neg_neg c, neg_smul, neg_pos] - exact smul_neg_iff_of_pos (neg_pos_of_neg hc) -#align smul_pos_iff_of_neg smul_pos_iff_of_neg - -#align smul_nonpos_of_nonpos_of_nonneg smul_nonpos_of_nonpos_of_nonneg - -theorem smul_nonneg_of_nonpos_of_nonpos (hc : c ≤ 0) (ha : a ≤ 0) : 0 ≤ c • a := - smul_nonpos_of_nonpos_of_nonneg (β := Mᵒᵈ) hc ha -#align smul_nonneg_of_nonpos_of_nonpos smul_nonneg_of_nonpos_of_nonpos - -alias ⟨_, smul_pos_of_neg_of_neg⟩ := smul_pos_iff_of_neg -#align smul_pos_of_neg_of_neg smul_pos_of_neg_of_neg - -#align smul_neg_of_pos_of_neg smul_neg_of_pos_of_neg -#align smul_neg_of_neg_of_pos smul_neg_of_neg_of_pos - -theorem antitone_smul_left (hc : c ≤ 0) : Antitone (SMul.smul c : M → M) := fun _ _ h => - smul_le_smul_of_nonpos h hc -#align antitone_smul_left antitone_smul_left - -theorem strict_anti_smul_left (hc : c < 0) : StrictAnti (SMul.smul c : M → M) := fun _ _ h => - smul_lt_smul_of_neg h hc -#align strict_anti_smul_left strict_anti_smul_left - -/-- Binary **rearrangement inequality**. -/ -theorem smul_add_smul_le_smul_add_smul [ContravariantClass M M (· + ·) (· ≤ ·)] {a b : k} {c d : M} - (hab : a ≤ b) (hcd : c ≤ d) : a • d + b • c ≤ a • c + b • d := by - obtain ⟨b, rfl⟩ := exists_add_of_le hab - obtain ⟨d, rfl⟩ := exists_add_of_le hcd - rw [smul_add, add_right_comm, smul_add, ← add_assoc, add_smul _ _ d] - rw [le_add_iff_nonneg_right] at hab hcd - exact add_le_add_left (le_add_of_nonneg_right <| smul_nonneg hab hcd) _ -#align smul_add_smul_le_smul_add_smul smul_add_smul_le_smul_add_smul - -/-- Binary **rearrangement inequality**. -/ -theorem smul_add_smul_le_smul_add_smul' [ContravariantClass M M (· + ·) (· ≤ ·)] {a b : k} {c d : M} - (hba : b ≤ a) (hdc : d ≤ c) : a • d + b • c ≤ a • c + b • d := by - rw [add_comm (a • d), add_comm (a • c)] - exact smul_add_smul_le_smul_add_smul hba hdc -#align smul_add_smul_le_smul_add_smul' smul_add_smul_le_smul_add_smul' - -/-- Binary strict **rearrangement inequality**. -/ -theorem smul_add_smul_lt_smul_add_smul [CovariantClass M M (· + ·) (· < ·)] - [ContravariantClass M M (· + ·) (· < ·)] {a b : k} {c d : M} (hab : a < b) (hcd : c < d) : - a • d + b • c < a • c + b • d := by - obtain ⟨b, rfl⟩ := exists_add_of_le hab.le - obtain ⟨d, rfl⟩ := exists_add_of_le hcd.le - rw [smul_add, add_right_comm, smul_add, ← add_assoc, add_smul _ _ d] - rw [lt_add_iff_pos_right] at hab hcd - exact add_lt_add_left (lt_add_of_pos_right _ <| smul_pos hab hcd) _ -#align smul_add_smul_lt_smul_add_smul smul_add_smul_lt_smul_add_smul - -/-- Binary strict **rearrangement inequality**. -/ -theorem smul_add_smul_lt_smul_add_smul' [CovariantClass M M (· + ·) (· < ·)] - [ContravariantClass M M (· + ·) (· < ·)] {a b : k} {c d : M} (hba : b < a) (hdc : d < c) : - a • d + b • c < a • c + b • d := by - rw [add_comm (a • d), add_comm (a • c)] - exact smul_add_smul_lt_smul_add_smul hba hdc -#align smul_add_smul_lt_smul_add_smul' smul_add_smul_lt_smul_add_smul' - -end Ring - -section Field - -variable [LinearOrderedField k] [OrderedAddCommGroup M] [Module k M] [OrderedSMul k M] {a b : M} - {c : k} - -theorem smul_le_smul_iff_of_neg (hc : c < 0) : c • a ≤ c • b ↔ b ≤ a := by - rw [← neg_neg c, neg_smul, neg_smul (-c), neg_le_neg_iff] - exact smul_le_smul_iff_of_pos_left (neg_pos_of_neg hc) -#align smul_le_smul_iff_of_neg smul_le_smul_iff_of_neg - -theorem inv_smul_le_iff_of_neg (h : c < 0) : c⁻¹ • a ≤ b ↔ c • b ≤ a := by - rw [← smul_le_smul_iff_of_neg h, smul_inv_smul₀ h.ne] -#align inv_smul_le_iff_of_neg inv_smul_le_iff_of_neg - -theorem inv_smul_lt_iff_of_neg (h : c < 0) : c⁻¹ • a < b ↔ c • b < a := by - rw [← smul_lt_smul_iff_of_neg h, smul_inv_smul₀ h.ne] -#align inv_smul_lt_iff_of_neg inv_smul_lt_iff_of_neg - -theorem smul_inv_le_iff_of_neg (h : c < 0) : a ≤ c⁻¹ • b ↔ b ≤ c • a := by - rw [← smul_le_smul_iff_of_neg h, smul_inv_smul₀ h.ne] -#align smul_inv_le_iff_of_neg smul_inv_le_iff_of_neg - -theorem smul_inv_lt_iff_of_neg (h : c < 0) : a < c⁻¹ • b ↔ b < c • a := by - rw [← smul_lt_smul_iff_of_neg h, smul_inv_smul₀ h.ne] -#align smul_inv_lt_iff_of_neg smul_inv_lt_iff_of_neg - -variable (M) - -/-- Left scalar multiplication as an order isomorphism. -/ -@[simps] -def OrderIso.smulLeftDual {c : k} (hc : c < 0) : M ≃o Mᵒᵈ where - toFun b := OrderDual.toDual (c • b) - invFun b := c⁻¹ • OrderDual.ofDual b - left_inv := inv_smul_smul₀ hc.ne - right_inv := smul_inv_smul₀ hc.ne - map_rel_iff' := (@OrderDual.toDual_le_toDual M).trans <| smul_le_smul_iff_of_neg hc -#align order_iso.smul_left_dual OrderIso.smulLeftDual - -end Field - -/-! ### Upper/lower bounds -/ - - -section OrderedRing - -variable [OrderedRing k] [OrderedAddCommGroup M] [Module k M] [OrderedSMul k M] {s : Set M} {c : k} - -theorem smul_lowerBounds_subset_upperBounds_smul (hc : c ≤ 0) : - c • lowerBounds s ⊆ upperBounds (c • s) := - (antitone_smul_left hc).image_lowerBounds_subset_upperBounds_image -#align smul_lower_bounds_subset_upper_bounds_smul smul_lowerBounds_subset_upperBounds_smul - -theorem smul_upperBounds_subset_lowerBounds_smul (hc : c ≤ 0) : - c • upperBounds s ⊆ lowerBounds (c • s) := - (antitone_smul_left hc).image_upperBounds_subset_lowerBounds_image -#align smul_upper_bounds_subset_lower_bounds_smul smul_upperBounds_subset_lowerBounds_smul - -theorem BddBelow.smul_of_nonpos (hc : c ≤ 0) (hs : BddBelow s) : BddAbove (c • s) := - (antitone_smul_left hc).map_bddBelow hs -#align bdd_below.smul_of_nonpos BddBelow.smul_of_nonpos - -theorem BddAbove.smul_of_nonpos (hc : c ≤ 0) (hs : BddAbove s) : BddBelow (c • s) := - (antitone_smul_left hc).map_bddAbove hs -#align bdd_above.smul_of_nonpos BddAbove.smul_of_nonpos - -end OrderedRing - -section LinearOrderedRing -variable [LinearOrderedRing k] [LinearOrderedAddCommGroup M] [Module k M] [OrderedSMul k M] - {f : ι → k} {g : ι → M} {s : Set ι} {a a₁ a₂ : k} {b b₁ b₂ : M} - -theorem smul_max_of_nonpos (ha : a ≤ 0) (b₁ b₂ : M) : a • max b₁ b₂ = min (a • b₁) (a • b₂) := - (antitone_smul_left ha : Antitone (_ : M → M)).map_max -#align smul_max_of_nonpos smul_max_of_nonpos - -theorem smul_min_of_nonpos (ha : a ≤ 0) (b₁ b₂ : M) : a • min b₁ b₂ = max (a • b₁) (a • b₂) := - (antitone_smul_left ha : Antitone (_ : M → M)).map_min -#align smul_min_of_nonpos smul_min_of_nonpos - -lemma nonneg_and_nonneg_or_nonpos_and_nonpos_of_smul_nonneg (hab : 0 ≤ a • b) : - 0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0 := by - simp only [Decidable.or_iff_not_and_not, not_and, not_le] - refine fun ab nab ↦ hab.not_lt ?_ - obtain ha | rfl | ha := lt_trichotomy 0 a - exacts [smul_neg_of_pos_of_neg ha (ab ha.le), ((ab le_rfl).asymm (nab le_rfl)).elim, - smul_neg_of_neg_of_pos ha (nab ha.le)] - -lemma smul_nonneg_iff : 0 ≤ a • b ↔ 0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0 := - ⟨nonneg_and_nonneg_or_nonpos_and_nonpos_of_smul_nonneg, - fun h ↦ h.elim (and_imp.2 smul_nonneg) (and_imp.2 smul_nonneg_of_nonpos_of_nonpos)⟩ - -lemma smul_nonpos_iff : a • b ≤ 0 ↔ 0 ≤ a ∧ b ≤ 0 ∨ a ≤ 0 ∧ 0 ≤ b := by - rw [← neg_nonneg, ← smul_neg, smul_nonneg_iff, neg_nonneg, neg_nonpos] - -lemma smul_nonneg_iff_pos_imp_nonneg : 0 ≤ a • b ↔ (0 < a → 0 ≤ b) ∧ (0 < b → 0 ≤ a) := by - refine smul_nonneg_iff.trans ?_ - simp_rw [← not_le, ← or_iff_not_imp_left] - have := le_total a 0 - have := le_total b 0 - tauto - -lemma smul_nonneg_iff_neg_imp_nonpos : 0 ≤ a • b ↔ (a < 0 → b ≤ 0) ∧ (b < 0 → a ≤ 0) := by - rw [← neg_smul_neg, smul_nonneg_iff_pos_imp_nonneg]; simp only [neg_pos, neg_nonneg] - -lemma smul_nonpos_iff_pos_imp_nonpos : a • b ≤ 0 ↔ (0 < a → b ≤ 0) ∧ (b < 0 → 0 ≤ a) := by - rw [← neg_nonneg, ← smul_neg, smul_nonneg_iff_pos_imp_nonneg]; simp only [neg_pos, neg_nonneg] - -lemma smul_nonpos_iff_neg_imp_nonneg : a • b ≤ 0 ↔ (a < 0 → 0 ≤ b) ∧ (0 < b → a ≤ 0) := by - rw [← neg_nonneg, ← neg_smul, smul_nonneg_iff_pos_imp_nonneg]; simp only [neg_pos, neg_nonneg] - -end LinearOrderedRing - -section LinearOrderedField - -variable [LinearOrderedField k] [OrderedAddCommGroup M] [Module k M] [OrderedSMul k M] {s : Set M} - {c : k} - -@[simp] -theorem lowerBounds_smul_of_neg (hc : c < 0) : lowerBounds (c • s) = c • upperBounds s := - (OrderIso.smulLeftDual M hc).upperBounds_image -#align lower_bounds_smul_of_neg lowerBounds_smul_of_neg - -@[simp] -theorem upperBounds_smul_of_neg (hc : c < 0) : upperBounds (c • s) = c • lowerBounds s := - (OrderIso.smulLeftDual M hc).lowerBounds_image -#align upper_bounds_smul_of_neg upperBounds_smul_of_neg - -@[simp] -theorem bddBelow_smul_iff_of_neg (hc : c < 0) : BddBelow (c • s) ↔ BddAbove s := - (OrderIso.smulLeftDual M hc).bddAbove_image -#align bdd_below_smul_iff_of_neg bddBelow_smul_iff_of_neg - -@[simp] -theorem bddAbove_smul_iff_of_neg (hc : c < 0) : BddAbove (c • s) ↔ BddBelow s := - (OrderIso.smulLeftDual M hc).bddBelow_image -#align bdd_above_smul_iff_of_neg bddAbove_smul_iff_of_neg - -end LinearOrderedField diff --git a/Mathlib/Algebra/Order/Module/Defs.lean b/Mathlib/Algebra/Order/Module/Defs.lean index dc071e86d3c8d..0c711f3e82847 100644 --- a/Mathlib/Algebra/Order/Module/Defs.lean +++ b/Mathlib/Algebra/Order/Module/Defs.lean @@ -453,6 +453,7 @@ lemma smul_pos [PosSMulStrictMono α β] (ha : 0 < a) (hb : 0 < b) : 0 < a • b lemma smul_neg_of_pos_of_neg [PosSMulStrictMono α β] (ha : 0 < a) (hb : b < 0) : a • b < 0 := by simpa only [smul_zero] using smul_lt_smul_of_pos_left hb ha +#align smul_neg_of_pos_of_neg smul_neg_of_pos_of_neg @[simp] lemma smul_pos_iff_of_pos_left [PosSMulStrictMono α β] [PosSMulReflectLT α β] (ha : 0 < a) : @@ -460,6 +461,11 @@ lemma smul_pos_iff_of_pos_left [PosSMulStrictMono α β] [PosSMulReflectLT α β simpa only [smul_zero] using smul_lt_smul_iff_of_pos_left ha (b₁ := 0) (b₂ := b) #align smul_pos_iff_of_pos smul_pos_iff_of_pos_left +lemma smul_neg_iff_of_pos_left [PosSMulStrictMono α β] [PosSMulReflectLT α β] (ha : 0 < a) : + a • b < 0 ↔ b < 0 := by + simpa only [smul_zero] using smul_lt_smul_iff_of_pos_left ha (b₂ := (0 : β)) +#align smul_neg_iff_of_pos smul_neg_iff_of_pos_left + lemma smul_nonneg [PosSMulMono α β] (ha : 0 ≤ a) (hb : 0 ≤ b₁) : 0 ≤ a • b₁ := by simpa only [smul_zero] using smul_le_smul_of_nonneg_left hb ha #align smul_nonneg smul_nonneg @@ -468,7 +474,10 @@ lemma smul_nonpos_of_nonneg_of_nonpos [PosSMulMono α β] (ha : 0 ≤ a) (hb : b simpa only [smul_zero] using smul_le_smul_of_nonneg_left hb ha #align smul_nonpos_of_nonneg_of_nonpos smul_nonpos_of_nonneg_of_nonpos -lemma pos_of_smul_pos_right [PosSMulReflectLT α β] (h : 0 < a • b) (ha : 0 ≤ a) : 0 < b := +lemma pos_of_smul_pos_left [PosSMulReflectLT α β] (h : 0 < a • b) (ha : 0 ≤ a) : 0 < b := + lt_of_smul_lt_smul_left (by rwa [smul_zero]) ha + +lemma neg_of_smul_neg_left [PosSMulReflectLT α β] (h : a • b < 0) (ha : 0 ≤ a) : b < 0 := lt_of_smul_lt_smul_left (by rwa [smul_zero]) ha end Preorder @@ -485,6 +494,7 @@ lemma smul_pos' [SMulPosStrictMono α β] (ha : 0 < a) (hb : 0 < b) : 0 < a • lemma smul_neg_of_neg_of_pos [SMulPosStrictMono α β] (ha : a < 0) (hb : 0 < b) : a • b < 0 := by simpa only [zero_smul] using smul_lt_smul_of_pos_right ha hb +#align smul_neg_of_neg_of_pos smul_neg_of_neg_of_pos @[simp] lemma smul_pos_iff_of_pos_right [SMulPosStrictMono α β] [SMulPosReflectLT α β] (hb : 0 < b) : @@ -496,13 +506,17 @@ lemma smul_nonneg' [SMulPosMono α β] (ha : 0 ≤ a) (hb : 0 ≤ b₁) : 0 ≤ lemma smul_nonpos_of_nonpos_of_nonneg [SMulPosMono α β] (ha : a ≤ 0) (hb : 0 ≤ b) : a • b ≤ 0 := by simpa only [zero_smul] using smul_le_smul_of_nonneg_right ha hb +#align smul_nonpos_of_nonpos_of_nonneg smul_nonpos_of_nonpos_of_nonneg -lemma pos_of_smul_pos_left [SMulPosReflectLT α β] (h : 0 < a • b) (hb : 0 ≤ b) : 0 < a := +lemma pos_of_smul_pos_right [SMulPosReflectLT α β] (h : 0 < a • b) (hb : 0 ≤ b) : 0 < a := + lt_of_smul_lt_smul_right (by rwa [zero_smul]) hb + +lemma neg_of_smul_neg_right [SMulPosReflectLT α β] (h : a • b < 0) (hb : 0 ≤ b) : a < 0 := lt_of_smul_lt_smul_right (by rwa [zero_smul]) hb lemma pos_iff_pos_of_smul_pos [PosSMulReflectLT α β] [SMulPosReflectLT α β] (hab : 0 < a • b) : 0 < a ↔ 0 < b := - ⟨pos_of_smul_pos_right hab ∘ le_of_lt, pos_of_smul_pos_left hab ∘ le_of_lt⟩ + ⟨pos_of_smul_pos_left hab ∘ le_of_lt, pos_of_smul_pos_right hab ∘ le_of_lt⟩ end Preorder @@ -620,18 +634,12 @@ lemma neg_iff_neg_of_smul_pos [PosSMulMono α β] [SMulPosMono α β] (hab : 0 < a < 0 ↔ b < 0 := ⟨neg_of_smul_pos_right hab ∘ le_of_lt, neg_of_smul_pos_left hab ∘ le_of_lt⟩ -lemma neg_of_smul_neg_left [PosSMulMono α β] (h : a • b < 0) (ha : 0 ≤ a) : b < 0 := - lt_of_not_ge fun hb ↦ (smul_nonneg ha hb).not_lt h - lemma neg_of_smul_neg_left' [SMulPosMono α β] (h : a • b < 0) (ha : 0 ≤ a) : b < 0 := lt_of_not_ge fun hb ↦ (smul_nonneg' ha hb).not_lt h -lemma neg_of_smul_neg_right [PosSMulMono α β] (h : a • b < 0) (hb : 0 ≤ b) : a < 0 := +lemma neg_of_smul_neg_right' [PosSMulMono α β] (h : a • b < 0) (hb : 0 ≤ b) : a < 0 := lt_of_not_ge fun ha ↦ (smul_nonneg ha hb).not_lt h -lemma neg_of_smul_neg_right' [SMulPosMono α β] (h : a • b < 0) (hb : 0 ≤ b) : a < 0 := - lt_of_not_ge fun ha ↦ (smul_nonneg' ha hb).not_lt h - end LinearOrder end SMulWithZero @@ -723,17 +731,6 @@ lemma SMulPosReflectLE_iff_smulPosReflectLT : SMulPosReflectLE α β ↔ SMulPos end PartialOrder end Ring -section OrderedRing -variable [OrderedRing α] [OrderedAddCommGroup β] [Module α β] - -instance PosSMulMono.toSMulPosMono [PosSMulMono α β] : SMulPosMono α β where - elim _b hb a₁ a₂ ha := by rw [← sub_nonneg, ← sub_smul]; exact smul_nonneg (sub_nonneg.2 ha) hb - -instance PosSMulStrictMono.toSMulPosStrictMono [PosSMulStrictMono α β] : SMulPosStrictMono α β where - elim _b hb a₁ a₂ ha := by rw [← sub_pos, ← sub_smul]; exact smul_pos (sub_pos.2 ha) hb - -end OrderedRing - section GroupWithZero variable [GroupWithZero α] [Preorder α] [Preorder β] [MulAction α β] @@ -764,22 +761,6 @@ def OrderIso.smulRight [PosSMulMono α β] [PosSMulReflectLE α β] {a : α} (ha end GroupWithZero -section LinearOrderedSemifield -variable [LinearOrderedSemifield α] [AddCommGroup β] [PartialOrder β] - --- See note [lower instance priority] -instance (priority := 100) PosSMulMono.toPosSMulReflectLE [MulAction α β] [PosSMulMono α β] : - PosSMulReflectLE α β where - elim _a ha b₁ b₂ h := by simpa [ha.ne'] using smul_le_smul_of_nonneg_left h $ inv_nonneg.2 ha.le - --- See note [lower instance priority] -instance (priority := 100) PosSMulStrictMono.toPosSMulReflectLT [MulActionWithZero α β] - [PosSMulStrictMono α β] : PosSMulReflectLT α β := - PosSMulReflectLT.of_pos fun a ha b₁ b₂ h ↦ by - simpa [ha.ne'] using smul_lt_smul_of_pos_left h $ inv_pos.2 ha - -end LinearOrderedSemifield - namespace OrderDual section Left @@ -822,6 +803,232 @@ instance instSMulPosReflectLE [SMulPosReflectLE α β] : SMulPosReflectLE α β end Right end OrderDual +section OrderedRing +variable [OrderedRing α] + +section OrderedAddCommGroup +variable [OrderedAddCommGroup β] [Module α β] + +#noalign eq_of_smul_eq_smul_of_neg_of_le + +section PosSMulMono +variable [PosSMulMono α β] + +lemma smul_le_smul_of_nonpos (h : b₁ ≤ b₂) (ha : a ≤ 0) : a • b₂ ≤ a • b₁ := by + rw [← neg_neg a, neg_smul, neg_smul (-a), neg_le_neg_iff] + exact smul_le_smul_of_nonneg_left h (neg_nonneg_of_nonpos ha) +#align smul_le_smul_of_nonpos smul_le_smul_of_nonpos + +lemma antitone_smul_left (ha : a ≤ 0) : Antitone (SMul.smul a : β → β) := + fun _ _ h => smul_le_smul_of_nonpos h ha +#align antitone_smul_left antitone_smul_left + +instance PosSMulMono.toSMulPosMono : SMulPosMono α β where + elim _b hb a₁ a₂ ha := by rw [← sub_nonneg, ← sub_smul]; exact smul_nonneg (sub_nonneg.2 ha) hb + +end PosSMulMono + +section PosSMulStrictMono +variable [PosSMulStrictMono α β] + +lemma smul_lt_smul_of_neg (hb : b₁ < b₂) (ha : a < 0) : a • b₂ < a • b₁ := by + rw [← neg_neg a, neg_smul, neg_smul (-a), neg_lt_neg_iff] + exact smul_lt_smul_of_pos_left hb (neg_pos_of_neg ha) +#align smul_lt_smul_of_neg smul_lt_smul_of_neg + +lemma strict_anti_smul_left (ha : a < 0) : StrictAnti (SMul.smul a : β → β) := + fun _ _ h => smul_lt_smul_of_neg h ha +#align strict_anti_smul_left strict_anti_smul_left + +instance PosSMulStrictMono.toSMulPosStrictMono : SMulPosStrictMono α β where + elim _b hb a₁ a₂ ha := by rw [← sub_pos, ← sub_smul]; exact smul_pos (sub_pos.2 ha) hb + +end PosSMulStrictMono + +lemma le_of_smul_le_smul_of_neg [PosSMulReflectLE α β] (h : a • b₁ ≤ a • b₂) (ha : a < 0) : + b₂ ≤ b₁ := by + rw [← neg_neg a, neg_smul, neg_smul (-a), neg_le_neg_iff] at h + exact le_of_smul_le_smul_of_pos_left h $ neg_pos.2 ha + +lemma lt_of_smul_lt_smul_of_nonpos [PosSMulReflectLT α β] (h : a • b₁ < a • b₂) (ha : a ≤ 0) : + b₂ < b₁ := by + rw [← neg_neg a, neg_smul, neg_smul (-a), neg_lt_neg_iff] at h + exact lt_of_smul_lt_smul_of_nonneg_left h (neg_nonneg_of_nonpos ha) +#align lt_of_smul_lt_smul_of_nonpos lt_of_smul_lt_smul_of_nonpos + +lemma smul_nonneg_of_nonpos_of_nonpos [SMulPosMono α β] (ha : a ≤ 0) (hb : b ≤ 0) : 0 ≤ a • b := + smul_nonpos_of_nonpos_of_nonneg (β := βᵒᵈ) ha hb +#align smul_nonneg_of_nonpos_of_nonpos smul_nonneg_of_nonpos_of_nonpos + +lemma smul_le_smul_iff_of_neg [PosSMulMono α β] [PosSMulReflectLE α β] (ha : a < 0) : + a • b₁ ≤ a • b₂ ↔ b₂ ≤ b₁ := by + rw [← neg_neg a, neg_smul, neg_smul (-a), neg_le_neg_iff] + exact smul_le_smul_iff_of_pos_left (neg_pos_of_neg ha) +#align smul_le_smul_iff_of_neg smul_le_smul_iff_of_neg + +section PosSMulStrictMono +variable [PosSMulStrictMono α β] [PosSMulReflectLT α β] + +lemma smul_lt_smul_iff_of_neg (ha : a < 0) : a • b₁ < a • b₂ ↔ b₂ < b₁ := by + rw [← neg_neg a, neg_smul, neg_smul (-a), neg_lt_neg_iff] + exact smul_lt_smul_iff_of_pos_left (neg_pos_of_neg ha) +#align smul_lt_smul_iff_of_neg smul_lt_smul_iff_of_neg + +lemma smul_pos_iff_of_neg (ha : a < 0) : 0 < a • b₁ ↔ b₁ < 0 := by + simpa only [smul_zero] using smul_lt_smul_iff_of_neg ha (b₁ := (0 : β)) +#align smul_pos_iff_of_neg smul_pos_iff_of_neg + +alias ⟨_, smul_pos_of_neg_of_neg⟩ := smul_pos_iff_of_neg +#align smul_pos_of_neg_of_neg smul_pos_of_neg_of_neg + +lemma smul_neg_iff_of_neg (ha : a < 0) : a • b₁ < 0 ↔ 0 < b₁ := by + simpa only [smul_zero] using smul_lt_smul_iff_of_neg ha (b₂ := (0 : β)) +#align smul_neg_iff_of_neg smul_neg_iff_of_neg + +end PosSMulStrictMono + +/-- Binary **rearrangement inequality**. -/ +lemma smul_add_smul_le_smul_add_smul [PosSMulMono α β] [ContravariantClass β β (· + ·) (· ≤ ·)] + {b₁ b₂ : α} {a d : β} (hab : b₁ ≤ b₂) (hcd : a ≤ d) : b₁ • d + b₂ • a ≤ b₁ • a + b₂ • d := by + obtain ⟨b₂, rfl⟩ := exists_add_of_le hab + obtain ⟨d, rfl⟩ := exists_add_of_le hcd + rw [smul_add, add_right_comm, smul_add, ← add_assoc, add_smul _ _ d] + rw [le_add_iff_nonneg_right] at hab hcd + exact add_le_add_left (le_add_of_nonneg_right <| smul_nonneg hab hcd) _ +#align smul_add_smul_le_smul_add_smul smul_add_smul_le_smul_add_smul + +/-- Binary **rearrangement inequality**. -/ +lemma smul_add_smul_le_smul_add_smul' [PosSMulMono α β] [ContravariantClass β β (· + ·) (· ≤ ·)] + {b₁ b₂ : α} {a d : β} (hba : b₂ ≤ b₁) (hdc : d ≤ a) : b₁ • d + b₂ • a ≤ b₁ • a + b₂ • d := by + rw [add_comm (b₁ • d), add_comm (b₁ • a)] + exact smul_add_smul_le_smul_add_smul hba hdc +#align smul_add_smul_le_smul_add_smul' smul_add_smul_le_smul_add_smul' + +/-- Binary strict **rearrangement inequality**. -/ +lemma smul_add_smul_lt_smul_add_smul [PosSMulStrictMono α β] [CovariantClass β β (· + ·) (· < ·)] + [ContravariantClass β β (· + ·) (· < ·)] {b₁ b₂ : α} {a d : β} (hab : b₁ < b₂) (hcd : a < d) : + b₁ • d + b₂ • a < b₁ • a + b₂ • d := by + obtain ⟨b₂, rfl⟩ := exists_add_of_le hab.le + obtain ⟨d, rfl⟩ := exists_add_of_le hcd.le + rw [smul_add, add_right_comm, smul_add, ← add_assoc, add_smul _ _ d] + rw [lt_add_iff_pos_right] at hab hcd + exact add_lt_add_left (lt_add_of_pos_right _ <| smul_pos hab hcd) _ +#align smul_add_smul_lt_smul_add_smul smul_add_smul_lt_smul_add_smul + +/-- Binary strict **rearrangement inequality**. -/ +lemma smul_add_smul_lt_smul_add_smul' [PosSMulStrictMono α β] [CovariantClass β β (· + ·) (· < ·)] + [ContravariantClass β β (· + ·) (· < ·)] {b₁ b₂ : α} {a d : β} (hba : b₂ < b₁) (hdc : d < a) : + b₁ • d + b₂ • a < b₁ • a + b₂ • d := by + rw [add_comm (b₁ • d), add_comm (b₁ • a)] + exact smul_add_smul_lt_smul_add_smul hba hdc +#align smul_add_smul_lt_smul_add_smul' smul_add_smul_lt_smul_add_smul' + +end OrderedAddCommGroup + +section LinearOrderedAddCommGroup +variable [LinearOrderedAddCommGroup β] [Module α β] [PosSMulMono α β] {a : α} {b b₁ b₂ : β} + +lemma smul_max_of_nonpos (ha : a ≤ 0) (b₁ b₂ : β) : a • max b₁ b₂ = min (a • b₁) (a • b₂) := + (antitone_smul_left ha : Antitone (_ : β → β)).map_max +#align smul_max_of_nonpos smul_max_of_nonpos + +lemma smul_min_of_nonpos (ha : a ≤ 0) (b₁ b₂ : β) : a • min b₁ b₂ = max (a • b₁) (a • b₂) := + (antitone_smul_left ha : Antitone (_ : β → β)).map_min +#align smul_min_of_nonpos smul_min_of_nonpos + +end LinearOrderedAddCommGroup +end OrderedRing + +section LinearOrderedRing +variable [LinearOrderedRing α] [LinearOrderedAddCommGroup β] [Module α β] [PosSMulStrictMono α β] + {a : α} {b : β} + +lemma nonneg_and_nonneg_or_nonpos_and_nonpos_of_smul_nonneg (hab : 0 ≤ a • b) : + 0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0 := by + simp only [Decidable.or_iff_not_and_not, not_and, not_le] + refine fun ab nab ↦ hab.not_lt ?_ + obtain ha | rfl | ha := lt_trichotomy 0 a + exacts [smul_neg_of_pos_of_neg ha (ab ha.le), ((ab le_rfl).asymm (nab le_rfl)).elim, + smul_neg_of_neg_of_pos ha (nab ha.le)] + +lemma smul_nonneg_iff : 0 ≤ a • b ↔ 0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0 := + ⟨nonneg_and_nonneg_or_nonpos_and_nonpos_of_smul_nonneg, + fun h ↦ h.elim (and_imp.2 smul_nonneg) (and_imp.2 smul_nonneg_of_nonpos_of_nonpos)⟩ + +lemma smul_nonpos_iff : a • b ≤ 0 ↔ 0 ≤ a ∧ b ≤ 0 ∨ a ≤ 0 ∧ 0 ≤ b := by + rw [← neg_nonneg, ← smul_neg, smul_nonneg_iff, neg_nonneg, neg_nonpos] + +lemma smul_nonneg_iff_pos_imp_nonneg : 0 ≤ a • b ↔ (0 < a → 0 ≤ b) ∧ (0 < b → 0 ≤ a) := + smul_nonneg_iff.trans $ by + simp_rw [← not_le, ← or_iff_not_imp_left]; have := le_total a 0; have := le_total b 0; tauto + +lemma smul_nonneg_iff_neg_imp_nonpos : 0 ≤ a • b ↔ (a < 0 → b ≤ 0) ∧ (b < 0 → a ≤ 0) := by + rw [← neg_smul_neg, smul_nonneg_iff_pos_imp_nonneg]; simp only [neg_pos, neg_nonneg] + +lemma smul_nonpos_iff_pos_imp_nonpos : a • b ≤ 0 ↔ (0 < a → b ≤ 0) ∧ (b < 0 → 0 ≤ a) := by + rw [← neg_nonneg, ← smul_neg, smul_nonneg_iff_pos_imp_nonneg]; simp only [neg_pos, neg_nonneg] + +lemma smul_nonpos_iff_neg_imp_nonneg : a • b ≤ 0 ↔ (a < 0 → 0 ≤ b) ∧ (0 < b → a ≤ 0) := by + rw [← neg_nonneg, ← neg_smul, smul_nonneg_iff_pos_imp_nonneg]; simp only [neg_pos, neg_nonneg] + +end LinearOrderedRing + +section LinearOrderedSemifield +variable [LinearOrderedSemifield α] [AddCommGroup β] [PartialOrder β] + +-- See note [lower instance priority] +instance (priority := 100) PosSMulMono.toPosSMulReflectLE [MulAction α β] [PosSMulMono α β] : + PosSMulReflectLE α β where + elim _a ha b₁ b₂ h := by simpa [ha.ne'] using smul_le_smul_of_nonneg_left h $ inv_nonneg.2 ha.le + +-- See note [lower instance priority] +instance (priority := 100) PosSMulStrictMono.toPosSMulReflectLT [MulActionWithZero α β] + [PosSMulStrictMono α β] : PosSMulReflectLT α β := + PosSMulReflectLT.of_pos fun a ha b₁ b₂ h ↦ by + simpa [ha.ne'] using smul_lt_smul_of_pos_left h $ inv_pos.2 ha + +end LinearOrderedSemifield + +section Field +variable [LinearOrderedField α] [OrderedAddCommGroup β] [Module α β] {a : α} {b₁ b₂ : β} + +section PosSMulMono +variable [PosSMulMono α β] + +lemma inv_smul_le_iff_of_neg (h : a < 0) : a⁻¹ • b₁ ≤ b₂ ↔ a • b₂ ≤ b₁ := by + rw [← smul_le_smul_iff_of_neg h, smul_inv_smul₀ h.ne] +#align inv_smul_le_iff_of_neg inv_smul_le_iff_of_neg + +lemma smul_inv_le_iff_of_neg (h : a < 0) : b₁ ≤ a⁻¹ • b₂ ↔ b₂ ≤ a • b₁ := by + rw [← smul_le_smul_iff_of_neg h, smul_inv_smul₀ h.ne] + +variable (β) + +/-- Left scalar multiplication as an order isomorphism. -/ +@[simps] +def OrderIso.smulLeftDual (ha : a < 0) : β ≃o βᵒᵈ where + toFun b₂ := OrderDual.toDual (a • b₂) + invFun b₂ := a⁻¹ • OrderDual.ofDual b₂ + left_inv := inv_smul_smul₀ ha.ne + right_inv := smul_inv_smul₀ ha.ne + map_rel_iff' := (@OrderDual.toDual_le_toDual β).trans <| smul_le_smul_iff_of_neg ha +#align order_iso.smul_left_dual OrderIso.smulLeftDual +#align smul_inv_le_iff_of_neg smul_inv_le_iff_of_neg + +end PosSMulMono + +variable [PosSMulStrictMono α β] + +lemma inv_smul_lt_iff_of_neg (h : a < 0) : a⁻¹ • b₁ < b₂ ↔ a • b₂ < b₁ := by + rw [← smul_lt_smul_iff_of_neg h, smul_inv_smul₀ h.ne] +#align inv_smul_lt_iff_of_neg inv_smul_lt_iff_of_neg + +lemma smul_inv_lt_iff_of_neg (h : a < 0) : b₁ < a⁻¹ • b₂ ↔ b₂ < a • b₁ := by + rw [← smul_lt_smul_iff_of_neg h, smul_inv_smul₀ h.ne] +#align smul_inv_lt_iff_of_neg smul_inv_lt_iff_of_neg + +end Field + namespace Prod end Prod @@ -994,3 +1201,4 @@ Those lemmas have been deprecated on the 2023/12/23. @[deprecated] alias OrderIso.smulLeft := OrderIso.smulRight @[deprecated] alias OrderIso.smulLeft_symm_apply := OrderIso.smulRight_symm_apply @[deprecated] alias OrderIso.smulLeft_apply := OrderIso.smulRight_apply +@[deprecated] alias smul_neg_iff_of_pos := smul_neg_iff_of_pos_left diff --git a/Mathlib/Algebra/Order/Module/Pointwise.lean b/Mathlib/Algebra/Order/Module/Pointwise.lean index df2102762d8cb..c0d4e0b66d4eb 100644 --- a/Mathlib/Algebra/Order/Module/Pointwise.lean +++ b/Mathlib/Algebra/Order/Module/Pointwise.lean @@ -61,3 +61,49 @@ variable [Preorder α] [Preorder β] [GroupWithZero α] [Zero β] [MulActionWith #align bdd_above_smul_iff_of_pos bddAbove_smul_iff_of_pos end + +section OrderedRing + +variable [OrderedRing α] [OrderedAddCommGroup β] [Module α β] [PosSMulMono α β] {s : Set β} {a : α} + +lemma smul_lowerBounds_subset_upperBounds_smul (ha : a ≤ 0) : + a • lowerBounds s ⊆ upperBounds (a • s) := + (antitone_smul_left ha).image_lowerBounds_subset_upperBounds_image +#align smul_lower_bounds_subset_upper_bounds_smul smul_lowerBounds_subset_upperBounds_smul + +lemma smul_upperBounds_subset_lowerBounds_smul (ha : a ≤ 0) : + a • upperBounds s ⊆ lowerBounds (a • s) := + (antitone_smul_left ha).image_upperBounds_subset_lowerBounds_image +#align smul_upper_bounds_subset_lower_bounds_smul smul_upperBounds_subset_lowerBounds_smul + +lemma BddBelow.smul_of_nonpos (ha : a ≤ 0) (hs : BddBelow s) : BddAbove (a • s) := + (antitone_smul_left ha).map_bddBelow hs +#align bdd_below.smul_of_nonpos BddBelow.smul_of_nonpos + +lemma BddAbove.smul_of_nonpos (ha : a ≤ 0) (hs : BddAbove s) : BddBelow (a • s) := + (antitone_smul_left ha).map_bddAbove hs +#align bdd_above.smul_of_nonpos BddAbove.smul_of_nonpos + +end OrderedRing + +section LinearOrderedField +variable [LinearOrderedField α] [OrderedAddCommGroup β] [Module α β] [PosSMulMono α β] {s : Set β} + {a : α} + +@[simp] lemma lowerBounds_smul_of_neg (ha : a < 0) : lowerBounds (a • s) = a • upperBounds s := + (OrderIso.smulLeftDual β ha).upperBounds_image +#align lower_bounds_smul_of_neg lowerBounds_smul_of_neg + +@[simp] lemma upperBounds_smul_of_neg (ha : a < 0) : upperBounds (a • s) = a • lowerBounds s := + (OrderIso.smulLeftDual β ha).lowerBounds_image +#align upper_bounds_smul_of_neg upperBounds_smul_of_neg + +@[simp] lemma bddBelow_smul_iff_of_neg (ha : a < 0) : BddBelow (a • s) ↔ BddAbove s := + (OrderIso.smulLeftDual β ha).bddAbove_image +#align bdd_below_smul_iff_of_neg bddBelow_smul_iff_of_neg + +@[simp] lemma bddAbove_smul_iff_of_neg (ha : a < 0) : BddAbove (a • s) ↔ BddBelow s := + (OrderIso.smulLeftDual β ha).bddBelow_image +#align bdd_above_smul_iff_of_neg bddAbove_smul_iff_of_neg + +end LinearOrderedField diff --git a/Mathlib/Algebra/Order/Module/Synonym.lean b/Mathlib/Algebra/Order/Module/Synonym.lean index 9bba3eca08309..6cd27a45ddc60 100644 --- a/Mathlib/Algebra/Order/Module/Synonym.lean +++ b/Mathlib/Algebra/Order/Module/Synonym.lean @@ -22,11 +22,11 @@ are already defined in `Mathlib.Algebra.Group.OrderSynonym`. namespace OrderDual variable {α β γ : Type*} -instance instSMulWithZero [Zero α] [AddZeroClass β] [SMulWithZero α β] : SMulWithZero αᵒᵈ β where +instance instSMulWithZero [Zero α] [Zero β] [SMulWithZero α β] : SMulWithZero αᵒᵈ β where zero_smul := zero_smul α smul_zero := smul_zero (M := α) -instance instSMulWithZero' [Zero α] [AddZeroClass β] [SMulWithZero α β] : SMulWithZero α βᵒᵈ where +instance instSMulWithZero' [Zero α] [Zero β] [SMulWithZero α β] : SMulWithZero α βᵒᵈ where zero_smul := zero_smul _ (M := β) smul_zero := smul_zero (A := β) diff --git a/Mathlib/Algebra/Order/Monovary.lean b/Mathlib/Algebra/Order/Monovary.lean index dec508e80301d..73928ce9ff8cf 100644 --- a/Mathlib/Algebra/Order/Monovary.lean +++ b/Mathlib/Algebra/Order/Monovary.lean @@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Yaël Dillies -/ import Mathlib.Algebra.Order.Group.Defs -import Mathlib.Algebra.Order.Module +import Mathlib.Algebra.Order.Module.OrderedSMul import Mathlib.Algebra.Order.Monoid.MinMax import Mathlib.Order.Monotone.Monovary diff --git a/Mathlib/Algebra/Order/Nonneg/Module.lean b/Mathlib/Algebra/Order/Nonneg/Module.lean index 2ed7956593457..735e574795eda 100644 --- a/Mathlib/Algebra/Order/Nonneg/Module.lean +++ b/Mathlib/Algebra/Order/Nonneg/Module.lean @@ -5,7 +5,7 @@ Authors: Apurva Nakade -/ import Mathlib.Algebra.Order.Nonneg.Ring import Mathlib.Algebra.Module.Basic -import Mathlib.Algebra.Order.Module +import Mathlib.Algebra.Order.Module.OrderedSMul /-! # Modules over nonnegative elements diff --git a/Mathlib/Algebra/Order/Rearrangement.lean b/Mathlib/Algebra/Order/Rearrangement.lean index 69e3ffa2282e8..1174e8d0c058c 100644 --- a/Mathlib/Algebra/Order/Rearrangement.lean +++ b/Mathlib/Algebra/Order/Rearrangement.lean @@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Mantas Bakšys -/ import Mathlib.Algebra.BigOperators.Basic -import Mathlib.Algebra.Order.Module +import Mathlib.Algebra.Order.Module.OrderedSMul import Mathlib.Data.Prod.Lex import Mathlib.GroupTheory.Perm.Support import Mathlib.Order.Monotone.Monovary diff --git a/Mathlib/Analysis/Convex/Basic.lean b/Mathlib/Analysis/Convex/Basic.lean index 198231f37e2ff..14702e7480347 100644 --- a/Mathlib/Analysis/Convex/Basic.lean +++ b/Mathlib/Analysis/Convex/Basic.lean @@ -3,7 +3,7 @@ Copyright (c) 2019 Alexander Bentkamp. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Alexander Bentkamp, Yury Kudriashov, Yaël Dillies -/ -import Mathlib.Algebra.Order.Module +import Mathlib.Algebra.Order.Module.OrderedSMul import Mathlib.Analysis.Convex.Star import Mathlib.LinearAlgebra.AffineSpace.AffineSubspace diff --git a/Mathlib/Data/Real/Pointwise.lean b/Mathlib/Data/Real/Pointwise.lean index a7e358f1267e2..c5dcdbb88058e 100644 --- a/Mathlib/Data/Real/Pointwise.lean +++ b/Mathlib/Data/Real/Pointwise.lean @@ -3,7 +3,7 @@ Copyright (c) 2021 Yaël Dillies. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Yaël Dillies, Eric Wieser -/ -import Mathlib.Algebra.Order.Module +import Mathlib.Algebra.Order.Module.OrderedSMul import Mathlib.Algebra.Order.Module.Pointwise import Mathlib.Data.Real.Archimedean diff --git a/Mathlib/LinearAlgebra/AffineSpace/Ordered.lean b/Mathlib/LinearAlgebra/AffineSpace/Ordered.lean index d74b0b15cb839..fd7653f7081ba 100644 --- a/Mathlib/LinearAlgebra/AffineSpace/Ordered.lean +++ b/Mathlib/LinearAlgebra/AffineSpace/Ordered.lean @@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Yury G. Kudryashov -/ import Mathlib.Algebra.Order.Invertible -import Mathlib.Algebra.Order.Module +import Mathlib.Algebra.Order.Module.OrderedSMul import Mathlib.LinearAlgebra.AffineSpace.MidpointZero import Mathlib.LinearAlgebra.AffineSpace.Slope import Mathlib.Tactic.FieldSimp