feat(analysis/convex): convex sets and functions (#834)

Author: abentkamp

src/algebra/module.lean

@@ -171,6 +171,28 @@ def mk' (f : β → γ) (H : is_linear_map α f) : β →ₗ γ := {to_fun := f,
 @[simp] theorem mk'_apply {f : β → γ} (H : is_linear_map α f) (x : β) :
   mk' f H x = f x := rfl
 
+lemma is_linear_map_neg :
+  is_linear_map α (λ (z : β), -z) :=
+is_linear_map.mk neg_add (λ x y, (smul_neg x y).symm)
+
+lemma is_linear_map_smul {α R : Type*} [add_comm_group α] [comm_ring R] [module R α] (c : R):
+  is_linear_map R (λ (z : α), c • z) :=
+begin
+  refine is_linear_map.mk (smul_add c) _,
+  intros _ _,
+  simp [smul_smul],
+  ac_refl
+end
+
+--TODO: move
+lemma is_linear_map_smul' {α R : Type*} [add_comm_group α] [comm_ring R] [module R α] (a : α):
+  is_linear_map R (λ (c : R), c • a) :=
+begin
+  refine is_linear_map.mk (λ x y, add_smul x y a) _,
+  intros _ _,
+  simp [smul_smul]
+end
+
 end is_linear_map
 
 /-- A submodule of a module is one which is closed under vector operations.