Commit 2024-08-05 13:16 fcfce357

View on Github →

chore: remove some open Classical, part 3 (#15417) See #15371.

Estimated changes

modified theorem BoxIntegral.integral_neg
modified theorem dslope_of_ne
modified theorem dslope_same
modified theorem IsLocalMax.deriv_eq_zero
modified theorem IsLocalMax.fderiv_eq_zero
modified theorem IsLocalMin.deriv_eq_zero
modified theorem IsLocalMin.fderiv_eq_zero
modified theorem lp.inner_single_left
modified theorem lp.inner_single_right