Theorem UniqueDiffWithinAt.of_real

Modification history

2025-06-12 14:04
Mathlib/Analysis/RCLike/TangentCone.lean
feat: unique differentiability over R implies unique differentiability over C (#25808)
Added UniqueDiffWithinAt.of_realView on Github →