Documentation

Mathlib.Algebra.Order.SMul

Ordered scalar product #

In this file we define

Implementation notes #

References #

Tags #

ordered module, ordered scalar, ordered smul, ordered action, ordered vector space

class OrderedSMul (R : Type u_1) (M : Type u_2) [inst : OrderedSemiring R] [inst : OrderedAddCommMonoid M] [inst : SMulWithZero R M] :
  • Scalar multiplication by positive elements preserves the order.

    smul_lt_smul_of_pos : ∀ {a b : M} {c : R}, a < b0 < cc a < c b
  • If c • a < c • b for some positive c, then a < b.

    lt_of_smul_lt_smul_of_pos : ∀ {a b : M} {c : R}, c a < c b0 < ca < b

The ordered scalar product property is when an ordered additive commutative monoid with a partial order has a scalar multiplication which is compatible with the order.

Instances
    instance OrderDual.instSMulWithZeroOrderDualInstZeroOrderDualToZero {R : Type u_1} {M : Type u_2} [inst : Zero R] [inst : AddZeroClass M] [inst : SMulWithZero R M] :
    Equations
    • OrderDual.instSMulWithZeroOrderDualInstZeroOrderDualToZero = let src := instSMulOrderDual; SMulWithZero.mk (_ : ∀ (m : Mᵒᵈ), 0 m = 0)
    instance OrderDual.instMulActionOrderDual {R : Type u_1} {M : Type u_2} [inst : Monoid R] [inst : MulAction R M] :
    Equations
    Equations
    • One or more equations did not get rendered due to their size.
    Equations
    theorem smul_lt_smul_of_pos {R : Type u_2} {M : Type u_1} [inst : OrderedSemiring R] [inst : OrderedAddCommMonoid M] [inst : SMulWithZero R M] [inst : OrderedSMul R M] {a : M} {b : M} {c : R} :
    a < b0 < cc a < c b
    theorem smul_le_smul_of_nonneg {R : Type u_2} {M : Type u_1} [inst : OrderedSemiring R] [inst : OrderedAddCommMonoid M] [inst : SMulWithZero R M] [inst : OrderedSMul R M] {a : M} {b : M} {c : R} (h₁ : a b) (h₂ : 0 c) :
    c a c b
    theorem smul_nonneg {R : Type u_1} {M : Type u_2} [inst : OrderedSemiring R] [inst : OrderedAddCommMonoid M] [inst : SMulWithZero R M] [inst : OrderedSMul R M] {a : M} {c : R} (hc : 0 c) (ha : 0 a) :
    0 c a
    theorem smul_nonpos_of_nonneg_of_nonpos {R : Type u_1} {M : Type u_2} [inst : OrderedSemiring R] [inst : OrderedAddCommMonoid M] [inst : SMulWithZero R M] [inst : OrderedSMul R M] {a : M} {c : R} (hc : 0 c) (ha : a 0) :
    c a 0
    theorem eq_of_smul_eq_smul_of_pos_of_le {R : Type u_2} {M : Type u_1} [inst : OrderedSemiring R] [inst : OrderedAddCommMonoid M] [inst : SMulWithZero R M] [inst : OrderedSMul R M] {a : M} {b : M} {c : R} (h₁ : c a = c b) (hc : 0 < c) (hle : a b) :
    a = b
    theorem lt_of_smul_lt_smul_of_nonneg {R : Type u_2} {M : Type u_1} [inst : OrderedSemiring R] [inst : OrderedAddCommMonoid M] [inst : SMulWithZero R M] [inst : OrderedSMul R M] {a : M} {b : M} {c : R} (h : c a < c b) (hc : 0 c) :
    a < b
    theorem smul_lt_smul_iff_of_pos {R : Type u_1} {M : Type u_2} [inst : OrderedSemiring R] [inst : OrderedAddCommMonoid M] [inst : SMulWithZero R M] [inst : OrderedSMul R M] {a : M} {b : M} {c : R} (hc : 0 < c) :
    c a < c b a < b
    theorem smul_pos_iff_of_pos {R : Type u_1} {M : Type u_2} [inst : OrderedSemiring R] [inst : OrderedAddCommMonoid M] [inst : SMulWithZero R M] [inst : OrderedSMul R M] {a : M} {c : R} (hc : 0 < c) :
    0 < c a 0 < a
    theorem smul_pos {R : Type u_1} {M : Type u_2} [inst : OrderedSemiring R] [inst : OrderedAddCommMonoid M] [inst : SMulWithZero R M] [inst : OrderedSMul R M] {a : M} {c : R} (hc : 0 < c) :
    0 < a0 < c a

    Alias of the reverse direction of smul_pos_iff_of_pos.

    theorem monotone_smul_left {R : Type u_1} {M : Type u_2} [inst : OrderedSemiring R] [inst : OrderedAddCommMonoid M] [inst : SMulWithZero R M] [inst : OrderedSMul R M] {c : R} (hc : 0 c) :
    theorem strictMono_smul_left {R : Type u_1} {M : Type u_2} [inst : OrderedSemiring R] [inst : OrderedAddCommMonoid M] [inst : SMulWithZero R M] [inst : OrderedSMul R M] {c : R} (hc : 0 < c) :
    theorem smul_lowerBounds_subset_lowerBounds_smul {R : Type u_1} {M : Type u_2} [inst : OrderedSemiring R] [inst : OrderedAddCommMonoid M] [inst : SMulWithZero R M] [inst : OrderedSMul R M] {s : Set M} {c : R} (hc : 0 c) :
    theorem smul_upperBounds_subset_upperBounds_smul {R : Type u_1} {M : Type u_2} [inst : OrderedSemiring R] [inst : OrderedAddCommMonoid M] [inst : SMulWithZero R M] [inst : OrderedSMul R M] {s : Set M} {c : R} (hc : 0 c) :
    theorem BddBelow.smul_of_nonneg {R : Type u_2} {M : Type u_1} [inst : OrderedSemiring R] [inst : OrderedAddCommMonoid M] [inst : SMulWithZero R M] [inst : OrderedSMul R M] {s : Set M} {c : R} (hs : BddBelow s) (hc : 0 c) :
    theorem BddAbove.smul_of_nonneg {R : Type u_2} {M : Type u_1} [inst : OrderedSemiring R] [inst : OrderedAddCommMonoid M] [inst : SMulWithZero R M] [inst : OrderedSMul R M] {s : Set M} {c : R} (hs : BddAbove s) (hc : 0 c) :
    theorem OrderedSMul.mk'' {𝕜 : Type u_1} {M : Type u_2} [inst : OrderedSemiring 𝕜] [inst : LinearOrderedAddCommMonoid M] [inst : SMulWithZero 𝕜 M] (h : ∀ ⦃c : 𝕜⦄, 0 < cStrictMono fun a => c a) :

    To prove that a linear ordered monoid is an ordered module, it suffices to verify only the first axiom of OrderedSMul.

    theorem OrderedSMul.mk' {𝕜 : Type u_2} {M : Type u_1} [inst : LinearOrderedSemifield 𝕜] [inst : OrderedAddCommMonoid M] [inst : MulActionWithZero 𝕜 M] (h : ∀ ⦃a b : M⦄ ⦃c : 𝕜⦄, a < b0 < cc a c b) :

    To prove that a vector space over a linear ordered field is ordered, it suffices to verify only the first axiom of OrderedSMul.

    instance Pi.orderedSMul {ι : Type u_1} {𝕜 : Type u_2} [inst : LinearOrderedSemifield 𝕜] {M : ιType u_3} [inst : (i : ι) → OrderedAddCommMonoid (M i)] [inst : (i : ι) → MulActionWithZero 𝕜 (M i)] [inst : ∀ (i : ι), OrderedSMul 𝕜 (M i)] :
    OrderedSMul 𝕜 ((i : ι) → M i)
    Equations
    instance Pi.orderedSMul' {ι : Type u_1} {𝕜 : Type u_2} {M : Type u_3} [inst : LinearOrderedSemifield 𝕜] [inst : OrderedAddCommMonoid M] [inst : MulActionWithZero 𝕜 M] [inst : OrderedSMul 𝕜 M] :
    OrderedSMul 𝕜 (ιM)
    Equations
    instance Pi.orderedSMul'' {ι : Type u_1} {𝕜 : Type u_2} [inst : LinearOrderedSemifield 𝕜] :
    OrderedSMul 𝕜 (ι𝕜)
    Equations
    theorem smul_le_smul_iff_of_pos {𝕜 : Type u_1} {M : Type u_2} [inst : LinearOrderedSemifield 𝕜] [inst : OrderedAddCommMonoid M] [inst : MulActionWithZero 𝕜 M] [inst : OrderedSMul 𝕜 M] {a : M} {b : M} {c : 𝕜} (hc : 0 < c) :
    c a c b a b
    theorem inv_smul_le_iff {𝕜 : Type u_1} {M : Type u_2} [inst : LinearOrderedSemifield 𝕜] [inst : OrderedAddCommMonoid M] [inst : MulActionWithZero 𝕜 M] [inst : OrderedSMul 𝕜 M] {a : M} {b : M} {c : 𝕜} (h : 0 < c) :
    c⁻¹ a b a c b
    theorem inv_smul_lt_iff {𝕜 : Type u_1} {M : Type u_2} [inst : LinearOrderedSemifield 𝕜] [inst : OrderedAddCommMonoid M] [inst : MulActionWithZero 𝕜 M] [inst : OrderedSMul 𝕜 M] {a : M} {b : M} {c : 𝕜} (h : 0 < c) :
    c⁻¹ a < b a < c b
    theorem le_inv_smul_iff {𝕜 : Type u_1} {M : Type u_2} [inst : LinearOrderedSemifield 𝕜] [inst : OrderedAddCommMonoid M] [inst : MulActionWithZero 𝕜 M] [inst : OrderedSMul 𝕜 M] {a : M} {b : M} {c : 𝕜} (h : 0 < c) :
    a c⁻¹ b c a b
    theorem lt_inv_smul_iff {𝕜 : Type u_1} {M : Type u_2} [inst : LinearOrderedSemifield 𝕜] [inst : OrderedAddCommMonoid M] [inst : MulActionWithZero 𝕜 M] [inst : OrderedSMul 𝕜 M] {a : M} {b : M} {c : 𝕜} (h : 0 < c) :
    a < c⁻¹ b c a < b
    @[simp]
    theorem OrderIso.smulLeft_symm_apply {𝕜 : Type u_1} (M : Type u_2) [inst : LinearOrderedSemifield 𝕜] [inst : OrderedAddCommMonoid M] [inst : MulActionWithZero 𝕜 M] [inst : OrderedSMul 𝕜 M] {c : 𝕜} (hc : 0 < c) (b : M) :
    @[simp]
    theorem OrderIso.smulLeft_apply {𝕜 : Type u_1} (M : Type u_2) [inst : LinearOrderedSemifield 𝕜] [inst : OrderedAddCommMonoid M] [inst : MulActionWithZero 𝕜 M] [inst : OrderedSMul 𝕜 M] {c : 𝕜} (hc : 0 < c) (b : M) :
    (RelIso.toRelEmbedding (OrderIso.smulLeft M hc)).toEmbedding b = c b
    def OrderIso.smulLeft {𝕜 : Type u_1} (M : Type u_2) [inst : LinearOrderedSemifield 𝕜] [inst : OrderedAddCommMonoid M] [inst : MulActionWithZero 𝕜 M] [inst : OrderedSMul 𝕜 M] {c : 𝕜} (hc : 0 < c) :
    M ≃o M

    Left scalar multiplication as an order isomorphism.

    Equations
    • One or more equations did not get rendered due to their size.
    @[simp]
    theorem lowerBounds_smul_of_pos {𝕜 : Type u_1} {M : Type u_2} [inst : LinearOrderedSemifield 𝕜] [inst : OrderedAddCommMonoid M] [inst : MulActionWithZero 𝕜 M] [inst : OrderedSMul 𝕜 M] {s : Set M} {c : 𝕜} (hc : 0 < c) :
    @[simp]
    theorem upperBounds_smul_of_pos {𝕜 : Type u_1} {M : Type u_2} [inst : LinearOrderedSemifield 𝕜] [inst : OrderedAddCommMonoid M] [inst : MulActionWithZero 𝕜 M] [inst : OrderedSMul 𝕜 M] {s : Set M} {c : 𝕜} (hc : 0 < c) :
    @[simp]
    theorem bddBelow_smul_iff_of_pos {𝕜 : Type u_1} {M : Type u_2} [inst : LinearOrderedSemifield 𝕜] [inst : OrderedAddCommMonoid M] [inst : MulActionWithZero 𝕜 M] [inst : OrderedSMul 𝕜 M] {s : Set M} {c : 𝕜} (hc : 0 < c) :
    @[simp]
    theorem bddAbove_smul_iff_of_pos {𝕜 : Type u_1} {M : Type u_2} [inst : LinearOrderedSemifield 𝕜] [inst : OrderedAddCommMonoid M] [inst : MulActionWithZero 𝕜 M] [inst : OrderedSMul 𝕜 M] {s : Set M} {c : 𝕜} (hc : 0 < c) :