Mathlib v3 is deprecated. Go to Mathlib v4

Theorem has_fderiv_at_filter.star

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 has_fderiv_at_filter.star View on Github →