Theorems · Inductive type · order theory
IsStrictOrderedModule
(α : Type u_1) → (β : Type u_2) → [SMul α β] → [Preorder α] → [Preorder β] → [Zero α] → [Zero β] → Prop
An ordered module is a module with a partial order such that scalar multiplication by a positive scalar and of a positive vector are both strictly monotone.
- Defined in
- Mathlib.Algebra.Order.Module.Defs
- Cited by
- 111 results in Mathlib
- Foundations
- Depth 1 from the axioms, rests on 4 definitions · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites1
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Preorderstatement · cited by 7,952
Cited by113
Results whose statement or proof uses this declaration.
- ConvexOn.map_sum_lestatement and proof · cited by 9
- gauge_smul_of_nonnegstatement and proof · cited by 7
- ConvexOn.exists_ge_of_mem_convexHullstatement and proof · cited by 5
- ConvexOn.map_centerMass_lestatement and proof · cited by 4
- lineMap_le_lineMap_iff_of_lt'statement and proof · cited by 4
- lineMap_lt_lineMap_iff_of_lt'statement and proof · cited by 4
- monovaryOn_iff_forall_smul_nonnegstatement and proof · cited by 4
- StrictConvexOn.map_sum_eq_iffstatement and proof · cited by 4
- ConvexOn.le_max_of_mem_segmentstatement and proof · cited by 3
- ConvexOn.smul'statement and proof · cited by 3
- monovaryOn_iff_smul_rearrangementstatement and proof · cited by 3
- StrictConvexOn.eq_of_le_map_sumstatement and proof · cited by 3