[Merged by Bors] - feat: Monotonicity of • on Finsupp

Mathlib/Data/DFinsupp/Order.lean

@@ -3,6 +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
 -/
+import Mathlib.Algebra.Order.Module.Defs
 import Mathlib.Data.DFinsupp.Basic
 
 #align_import data.dfinsupp.order from "leanprover-community/mathlib"@"1d29de43a5ba4662dd33b5cfeecfc2a27a5a8a29"
@@ -150,6 +151,42 @@ instance [∀ i, OrderedAddCommMonoid (α i)] [∀ i, ContravariantClass (α i)
     ContravariantClass (Π₀ i, α i) (Π₀ i, α i) (· + ·) (· ≤ ·) :=
   ⟨fun _ _ _ H i ↦ le_of_add_le_add_left (H i)⟩
 
+section Module
+variable {α : Type*} {β : ι → Type*} [Semiring α] [Preorder α] [∀ i, AddCommMonoid (β i)]
+  [∀ i, Preorder (β i)] [∀ i, Module α (β i)]
+
+instance instPosSMulMono [∀ i, PosSMulMono α (β i)] : PosSMulMono α (Π₀ i, β i) :=
+  PosSMulMono.lift _ coe_le_coe coe_smul
+
+instance instSMulPosMono [∀ i, SMulPosMono α (β i)] : SMulPosMono α (Π₀ i, β i) :=
+  SMulPosMono.lift _ coe_le_coe coe_smul coe_zero
+
+instance instPosSMulReflectLE [∀ i, PosSMulReflectLE α (β i)] : PosSMulReflectLE α (Π₀ i, β i) :=
+  PosSMulReflectLE.lift _ coe_le_coe coe_smul
+
+instance instSMulPosReflectLE [∀ i, SMulPosReflectLE α (β i)] : SMulPosReflectLE α (Π₀ i, β i) :=
+  SMulPosReflectLE.lift _ coe_le_coe coe_smul coe_zero
+
+end Module
+
+section Module
+variable {α : Type*} {β : ι → Type*} [Semiring α] [PartialOrder α] [∀ i, AddCommMonoid (β i)]
+  [∀ i, PartialOrder (β i)] [∀ i, Module α (β i)]
+
+instance instPosSMulStrictMono [∀ i, PosSMulStrictMono α (β i)] : PosSMulStrictMono α (Π₀ i, β i) :=
+  PosSMulStrictMono.lift _ coe_le_coe coe_smul
+
+instance instSMulPosStrictMono [∀ i, SMulPosStrictMono α (β i)] : SMulPosStrictMono α (Π₀ i, β i) :=
+  SMulPosStrictMono.lift _ coe_le_coe coe_smul coe_zero
+
+-- Note: There is no interesting instance for `PosSMulReflectLT α (Π₀ i, β i)` that's not already
+-- implied by the other instances
+
+instance instSMulPosReflectLT [∀ i, SMulPosReflectLT α (β i)] : SMulPosReflectLT α (Π₀ i, β i) :=
+  SMulPosReflectLT.lift _ coe_le_coe coe_smul coe_zero
+
+end Module
+
 section CanonicallyOrderedAddCommMonoid
 
 -- porting note: Split into 2 lines to satisfy the unusedVariables linter.

Mathlib/Data/Finsupp/Order.lean

@@ -3,7 +3,8 @@ Copyright (c) 2021 Johan Commelin. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johan Commelin, Aaron Anderson
 -/
-import Mathlib.Data.Finsupp.Defs
+import Mathlib.Algebra.Order.Module.Defs
+import Mathlib.Data.Finsupp.Basic
 
 #align_import data.finsupp.order from "leanprover-community/mathlib"@"1d29de43a5ba4662dd33b5cfeecfc2a27a5a8a29"
 
@@ -30,7 +31,7 @@ open BigOperators
 
 open Finset
 
-variable {ι α : Type*}
+variable {ι α β : Type*}
 
 namespace Finsupp
 
@@ -149,6 +150,39 @@ instance contravariantClass [OrderedAddCommMonoid α] [ContravariantClass α α
     ContravariantClass (ι →₀ α) (ι →₀ α) (· + ·) (· ≤ ·) :=
   ⟨fun _f _g _h H x => le_of_add_le_add_left <| H x⟩
 
+section SMulZeroClass
+variable [Zero α] [Preorder α] [Zero β] [Preorder β] [SMulZeroClass α β]
+
+instance instPosSMulMono [PosSMulMono α β] : PosSMulMono α (ι →₀ β) :=
+  PosSMulMono.lift _ coe_le_coe coe_smul
+
+instance instSMulPosMono [SMulPosMono α β] : SMulPosMono α (ι →₀ β) :=
+  SMulPosMono.lift _ coe_le_coe coe_smul coe_zero
+
+instance instPosSMulReflectLE [PosSMulReflectLE α β] : PosSMulReflectLE α (ι →₀ β) :=
+  PosSMulReflectLE.lift _ coe_le_coe coe_smul
+
+instance instSMulPosReflectLE [SMulPosReflectLE α β] : SMulPosReflectLE α (ι →₀ β) :=
+  SMulPosReflectLE.lift _ coe_le_coe coe_smul coe_zero
+
+end SMulZeroClass
+
+section SMulWithZero
+variable [Zero α] [PartialOrder α] [Zero β] [PartialOrder β] [SMulWithZero α β]
+
+instance instPosSMulStrictMono [PosSMulStrictMono α β] : PosSMulStrictMono α (ι →₀ β) :=
+  PosSMulStrictMono.lift _ coe_le_coe coe_smul
+
+instance instSMulPosStrictMono [SMulPosStrictMono α β] : SMulPosStrictMono α (ι →₀ β) :=
+  SMulPosStrictMono.lift _ coe_le_coe coe_smul coe_zero
+
+-- `PosSMulReflectLT α (ι →₀ β)` already follows from the other instances
+
+instance instSMulPosReflectLT [SMulPosReflectLT α β] : SMulPosReflectLT α (ι →₀ β) :=
+  SMulPosReflectLT.lift _ coe_le_coe coe_smul coe_zero
+
+end SMulWithZero
+
 section CanonicallyOrderedAddCommMonoid
 
 variable [CanonicallyOrderedAddCommMonoid α] {f g : ι →₀ α}