[Merged by Bors] - feat(LinearAlgebra/CliffordAlgebra): port SpinGroup

Mathlib.lean

@@ -2548,6 +2548,7 @@ import Mathlib.LinearAlgebra.CliffordAlgebra.Fold
 import Mathlib.LinearAlgebra.CliffordAlgebra.Grading
 import Mathlib.LinearAlgebra.CliffordAlgebra.Inversion
 import Mathlib.LinearAlgebra.CliffordAlgebra.Prod
+import Mathlib.LinearAlgebra.CliffordAlgebra.SpinGroup
 import Mathlib.LinearAlgebra.CliffordAlgebra.Star
 import Mathlib.LinearAlgebra.Coevaluation
 import Mathlib.LinearAlgebra.Contraction

Mathlib/Algebra/Module/Submodule/Pointwise.lean

@@ -240,6 +240,9 @@ theorem smul_mem_pointwise_smul (m : M) (a : α) (S : Submodule R M) : m ∈ S 
   (Set.smul_mem_smul_set : _ → _ ∈ a • (S : Set M))
 #align submodule.smul_mem_pointwise_smul Submodule.smul_mem_pointwise_smul
 
+theorem pointwise_smul_mono (a : α) : Monotone (fun S : Submodule R M => a • S) :=
+  fun _ _ => map_mono
+
 /-- See also `Submodule.smul_bot`. -/
 @[simp]
 theorem smul_bot' (a : α) : a • (⊥ : Submodule R M) = ⊥ :=