Mathlib Changelog
v4
Changelog
About
Github
Commit
2023-05-22 18:33
c851d271
View on Github →
feat: port Analysis.Calculus.Fderiv.Prod (
#4208
)
Estimated changes
Modified
Mathlib.lean
Created
Mathlib/Analysis/Calculus/FDeriv/Prod.lean
added
theorem
Differentiable.prod
added
theorem
DifferentiableAt.fderivWithin_prod
added
theorem
DifferentiableAt.fderiv_prod
added
theorem
DifferentiableAt.prod
added
theorem
DifferentiableOn.prod
added
theorem
DifferentiableWithinAt.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
differentiableWithinAt_fst
added
theorem
differentiableWithinAt_pi
added
theorem
differentiableWithinAt_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_prod_mk_left
added
theorem
hasFDerivAt_prod_mk_right
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