Commit 2025-06-12 14:04 cd302163

View on Github →

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

Estimated changes

Modified Mathlib.lean

Created Mathlib/Analysis/RCLike/TangentCone.lean

added theorem UniqueDiffOn.of_real

added theorem UniqueDiffWithinAt.of_real

added theorem tangentConeAt_real_subset_isRCLikeNormedField

added theorem uniqueDiffOn_convex_of_isRCLikeNormedField

added theorem uniqueDiffWithinAt_convex_of_isRCLikeNormedField