Theorem convex_RCLike_iff_convex_real

Modification history

2025-10-02 18:14
Mathlib/Analysis/RCLike/Lemmas.lean
feature(Analysis/Convex/Basic): Convexity and the algebra map (#29248) …
Added convex_RCLike_iff_convex_realView on Github →