One-dimensional derivatives on pi-types.

theorem hasDerivAt_update {𝕜 : Type u_1} {ι : Type u_2} [DecidableEq ι] [NontriviallyNormedField 𝕜] (x : ι → 𝕜) (i : ι) (y : 𝕜) : HasDerivAt (Function.update x i) (Pi.single i 1) y

theorem hasDerivAt_single {𝕜 : Type u_1} {ι : Type u_2} [DecidableEq ι] [NontriviallyNormedField 𝕜] (i : ι) (y : 𝕜) : HasDerivAt (Pi.single i) (Pi.single i 1) y

theorem deriv_update {𝕜 : Type u_1} {ι : Type u_2} [DecidableEq ι] [NontriviallyNormedField 𝕜] [Finite ι] (x : ι → 𝕜) (i : ι) (y : 𝕜) : deriv (Function.update x i) y = Pi.single i 1

theorem deriv_single {𝕜 : Type u_1} {ι : Type u_2} [DecidableEq ι] [NontriviallyNormedField 𝕜] [Finite ι] (i : ι) (y : 𝕜) : deriv (Pi.single i) y = Pi.single i 1