Mathlib v3 is deprecated. Go to Mathlib v4

Theorem differentiable_within_at_star_iff

Modification history

2023-05-23 12:33

src/analysis/calculus/fderiv/star.lean

feat(analysis/calculus/fderiv/star): derivative of star in star-modules over a trivial star-ring (#19038) …

Added differentiable_within_at_star_iff View on Github →