Commit 2025-10-02 18:14 18226f6c
View on Github →feature(Analysis/Convex/Basic): Convexity and the algebra map (#29248)
Let R and A be ordered rings, A an R-algebra and R, A, M a scalar tower. We provide sufficient conditions for an R-convex subset of M to be A-convex and for an A-convex subset of M to be R-convex.
These are used to show that, when K is RCLike and ℝ K E is a scalar tower, a set is K-convex if and only if it is ℝ-convex.
Used in #29258