Ordered vector spaces

@[instance 100]

instance PosSMulMono.toPosSMulReflectLE {𝕜 : Type u_1} {G : Type u_2} [Semifield 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [PartialOrder G] [MulAction 𝕜 G] [PosSMulMono 𝕜 G] : PosSMulReflectLE 𝕜 G

@[instance 100]

instance PosSMulStrictMono.toPosSMulReflectLT {𝕜 : Type u_1} {G : Type u_2} [Semifield 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [AddCommGroup G] [PartialOrder G] [MulActionWithZero 𝕜 G] [PosSMulStrictMono 𝕜 G] : PosSMulReflectLT 𝕜 G

theorem inv_smul_le_iff_of_neg {𝕜 : Type u_1} {G : Type u_2} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [AddCommGroup G] [PartialOrder G] [IsOrderedAddMonoid G] [Module 𝕜 G] {a : 𝕜} {b₁ b₂ : G} [PosSMulMono 𝕜 G] (h : a < 0) : a⁻¹ • b₁ ≤ b₂ ↔ a • b₂ ≤ b₁

theorem smul_inv_le_iff_of_neg {𝕜 : Type u_1} {G : Type u_2} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [AddCommGroup G] [PartialOrder G] [IsOrderedAddMonoid G] [Module 𝕜 G] {a : 𝕜} {b₁ b₂ : G} [PosSMulMono 𝕜 G] (h : a < 0) : b₁ ≤ a⁻¹ • b₂ ↔ b₂ ≤ a • b₁

def OrderIso.smulRightDual {𝕜 : Type u_1} (G : Type u_2) [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [AddCommGroup G] [PartialOrder G] [IsOrderedAddMonoid G] [Module 𝕜 G] {a : 𝕜} [PosSMulMono 𝕜 G] (ha : a < 0) : G ≃o Gᵒᵈ

Left scalar multiplication as an order isomorphism.

Equations

• OrderIso.smulRightDual G ha = { toEquiv := (Equiv.smulRight ⋯).trans OrderDual.toDual, map_rel_iff' := ⋯ }

@[simp]

theorem OrderIso.smulRightDual_symm_apply {𝕜 : Type u_1} (G : Type u_2) [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [AddCommGroup G] [PartialOrder G] [IsOrderedAddMonoid G] [Module 𝕜 G] {a : 𝕜} [PosSMulMono 𝕜 G] (ha : a < 0) (a✝ : Gᵒᵈ) : (RelIso.symm (smulRightDual G ha)) a✝ = a⁻¹ • OrderDual.ofDual a✝

@[simp]

theorem OrderIso.smulRightDual_apply {𝕜 : Type u_1} (G : Type u_2) [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [AddCommGroup G] [PartialOrder G] [IsOrderedAddMonoid G] [Module 𝕜 G] {a : 𝕜} [PosSMulMono 𝕜 G] (ha : a < 0) (a✝ : G) : (smulRightDual G ha) a✝ = a • OrderDual.toDual a✝

theorem inv_smul_lt_iff_of_neg {𝕜 : Type u_1} {G : Type u_2} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [AddCommGroup G] [PartialOrder G] [IsOrderedAddMonoid G] [Module 𝕜 G] {a : 𝕜} {b₁ b₂ : G} [PosSMulStrictMono 𝕜 G] (h : a < 0) : a⁻¹ • b₁ < b₂ ↔ a • b₂ < b₁

theorem smul_inv_lt_iff_of_neg {𝕜 : Type u_1} {G : Type u_2} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [AddCommGroup G] [PartialOrder G] [IsOrderedAddMonoid G] [Module 𝕜 G] {a : 𝕜} {b₁ b₂ : G} [PosSMulStrictMono 𝕜 G] (h : a < 0) : b₁ < a⁻¹ • b₂ ↔ b₂ < a • b₁

theorem Mathlib.Meta.Positivity.smul_nonneg_of_pos_of_nonneg {α : Type u_3} {β : Type u_4} [Zero α] [Zero β] [SMulZeroClass α β] [Preorder α] [Preorder β] [PosSMulMono α β] {a : α} {b : β} (ha : 0 < a) (hb : 0 ≤ b) : 0 ≤ a • b

theorem Mathlib.Meta.Positivity.smul_nonneg_of_nonneg_of_pos {α : Type u_3} {β : Type u_4} [Zero α] [Zero β] [SMulZeroClass α β] [Preorder α] [Preorder β] [PosSMulMono α β] {a : α} {b : β} (ha : 0 ≤ a) (hb : 0 < b) : 0 ≤ a • b

theorem Mathlib.Meta.Positivity.smul_nonneg_of_pos_of_pos {α : Type u_3} {β : Type u_4} [Zero α] [Zero β] [SMulZeroClass α β] [Preorder α] [Preorder β] [PosSMulMono α β] {a : α} {b : β} (ha : 0 < a) (hb : 0 < b) : 0 ≤ a • b

theorem Mathlib.Meta.Positivity.smul_ne_zero_of_pos_of_ne_zero {α : Type u_3} {β : Type u_4} [Semiring α] [IsDomain α] [AddCommMonoid β] [Module α β] [Module.IsTorsionFree α β] {a : α} {b : β} [Preorder α] (ha : 0 < a) (hb : b ≠ 0) : a • b ≠ 0

theorem Mathlib.Meta.Positivity.smul_ne_zero_of_ne_zero_of_pos {α : Type u_3} {β : Type u_4} [Semiring α] [IsDomain α] [AddCommMonoid β] [Module α β] [Module.IsTorsionFree α β] {a : α} {b : β} [Preorder β] (ha : a ≠ 0) (hb : 0 < b) : a • b ≠ 0

def Mathlib.Meta.Positivity.evalSMul : PositivityExt

Positivity extension for scalar multiplication.

Equations

• One or more equations did not get rendered due to their size.