Theorem uniqueDiffOn_convex_of_isRCLikeNormedField

Modification history

2025-06-12 14:04

Mathlib/Analysis/RCLike/TangentCone.lean

feat: unique differentiability over R implies unique differentiability over C (#25808)

Added uniqueDiffOn_convex_of_isRCLikeNormedField View on Github →