Commit 2023-05-22 18:33 c851d271

View on Github →

feat: port Analysis.Calculus.Fderiv.Prod (#4208)

Estimated changes

added theorem Differentiable.prod
added theorem DifferentiableAt.prod
added theorem DifferentiableOn.prod
added theorem HasFDerivAtFilter.prod
added theorem differentiableAt_fst
added theorem differentiableAt_pi
added theorem differentiableAt_snd
added theorem differentiableOn_fst
added theorem differentiableOn_pi
added theorem differentiableOn_snd
added theorem differentiable_fst
added theorem differentiable_pi
added theorem differentiable_snd
added theorem fderiv.fst
added theorem fderiv.snd
added theorem fderivWithin.fst
added theorem fderivWithin.snd
added theorem fderivWithin_fst
added theorem fderivWithin_pi
added theorem fderivWithin_snd
added theorem fderiv_fst
added theorem fderiv_pi
added theorem fderiv_snd
added theorem hasFDerivAtFilter_fst
added theorem hasFDerivAtFilter_pi'
added theorem hasFDerivAtFilter_pi
added theorem hasFDerivAtFilter_snd
added theorem hasFDerivAt_fst
added theorem hasFDerivAt_pi'
added theorem hasFDerivAt_pi
added theorem hasFDerivAt_snd
added theorem hasFDerivWithinAt_fst
added theorem hasFDerivWithinAt_pi'
added theorem hasFDerivWithinAt_pi
added theorem hasFDerivWithinAt_snd
added theorem hasStrictFDerivAt_fst
added theorem hasStrictFDerivAt_pi'
added theorem hasStrictFDerivAt_pi
added theorem hasStrictFDerivAt_snd