Theorem fderiv_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 fderiv_star View on Github →