better docs

Author: YaelDillies

Mathlib/Geometry/Convex/ConvexSpace/Module.lean

@@ -12,20 +12,13 @@ public import Mathlib.LinearAlgebra.AffineSpace.AffineMap
 /-!
 # Modules are convex spaces
 
-This file shows that every semimodule over an ordered semiring is a convex space.
+This file shows that every module over ordered coefficients is a convex space.
 
 ## Main declarations
 
 * `ConvexSpace.ofModule`: A semimodule space over a semiring is a convex space.
 * `convexSpaceSelf`: A semiring is a convex space over itself.
 * `IsModuleConvexSpace`: Predicate for a convex space and module structures to be compatible.
-
-## Implementation notes
-
-It is sadly impossible to make `ConvexSpace.ofModule` a global instance since it creates diamonds
-with structural instances such as `ConvexSpace R X → ConvexSpace R Y → ConvexSpace R (X × Y)`
-because `(∑ i, f i).fst = ∑ i, (f i).fst` isn't defeq, ultimately because `Finset.sum` isn't a field
-of `AddCommMonoid`.
 -/
 
 public section
@@ -36,7 +29,10 @@ variable {R M N I : Type*} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R]
 
 /-- Any semimodule over an ordered semiring is a convex space.
 
-This is not an instance because it creates a diamond. -/
+This is not an instance because it creates a diamond with structural instances such as
+`ConvexSpace R X → ConvexSpace R Y → ConvexSpace R (X × Y)` because
+`(∑ i, f i).fst = ∑ i, (f i).fst` isn't defeq, ultimately because `Finset.sum` isn't a field of
+`AddCommMonoid` but derived from them through recursion. -/
 @[expose, implicit_reducible]
 def ConvexSpace.ofModule : ConvexSpace R M where
   sConvexComb w := w.weights.sum fun m r ↦ r • m