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