Documentation on comp_linearmap

[BoltonBailey]

Just a quick issue as a reminder since I'm in the middle of something, but this docstring (and below) seems wrong: f is not the linear one, g is

mathlib4/Mathlib/Analysis/Convex/Function.lean

Lines 471 to 478 in 8666bd8

	/-- If `g` is convex on `s`, so is `(f ∘ g)` on `f ⁻¹' s` for a linear `f`. -/
	theorem ConvexOn.comp_linearMap {f : F → β} {s : Set F} (hf : ConvexOn 𝕜 s f) (g : E →ₗ[𝕜] F) :
	ConvexOn 𝕜 (g ⁻¹' s) (f ∘ g) :=
	⟨hf.1.linear_preimage _, fun x hx y hy a b ha hb hab =>
	calc
	f (g (a • x + b • y)) = f (a • g x + b • g y) := by rw [g.map_add, g.map_smul, g.map_smul]
	_ ≤ a • f (g x) + b • f (g y) := hf.2 hx hy ha hb hab⟩