Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-03-31 00:17 c5181d11

View on Github →

feat(*): more prod-related (continuous) linear maps and their derivatives (#2277)

  • feat(*): more prod-related (continuous) linear maps and their derivatives
  • Make R argument of continuous_linear_equiv.refl explicit

Estimated changes

added theorem differentiable.fst
added theorem differentiable.snd
added theorem differentiable_at.fst
added theorem differentiable_at.snd
added theorem differentiable_at_fst
added theorem differentiable_at_snd
added theorem differentiable_fst
added theorem differentiable_on.fst
added theorem differentiable_on.snd
added theorem differentiable_on_fst
added theorem differentiable_on_snd
added theorem differentiable_snd
added theorem fderiv.fst
added theorem fderiv.snd
added theorem fderiv_fst
added theorem fderiv_snd
added theorem fderiv_within.fst
added theorem fderiv_within.snd
added theorem fderiv_within_fst
added theorem fderiv_within_snd
added theorem has_fderiv_at.fst
added theorem has_fderiv_at.prod_map
added theorem has_fderiv_at.snd
added theorem has_fderiv_at_fst
added theorem has_fderiv_at_snd
added theorem linear_equiv.coe_prod
modified theorem nhds_basis_opens
added theorem continuous.prod_map