Theorem tangentConeAt_real_subset_isRCLikeNormedField

Modification history

2025-06-16 13:31
Mathlib/Analysis/RCLike/TangentCone.lean
chore: whitespace fixes (#25956) …
Modified tangentConeAt_real_subset_isRCLikeNormedFieldView on Github →
2025-06-12 14:04
Mathlib/Analysis/RCLike/TangentCone.lean
feat: unique differentiability over R implies unique differentiability over C (#25808)
Added tangentConeAt_real_subset_isRCLikeNormedFieldView on Github →