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₁

def Mathlib.Meta.Positivity.evalHSMul : PositivityExt

Positivity extension for HSMul, i.e. (_ • _).

Equations

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