English
The derivative of a multilinear map with respect to a family of inputs x on coordinates is given by summing over coordinates of the appropriate partial derivatives along those coordinates.
Русский
Производная мультиленейной карты по всем координатам равна сумме соответствующих частных производных по каждой координате.
LaTeX
$$def linearDeriv (f) (x) : ((i : ι) → M₁ i) →ₗ[R] M₂$$
Lean4
theorem domDomRestrict_aux_right {ι} [DecidableEq ι] (P : ι → Prop) [DecidablePred P] {M₁ : ι → Type*}
[DecidableEq { a // ¬P a }] (x : (i : { a // P a }) → M₁ i) (z : (i : { a // ¬P a }) → M₁ i) (i : { a : ι // ¬P a })
(c : M₁ i) :
(fun j ↦ if h : P j then x ⟨j, h⟩ else Function.update z i c ⟨j, h⟩) =
Function.update (fun j => if h : P j then x ⟨j, h⟩ else z ⟨j, h⟩) i c :=
by simpa only [dite_not] using domDomRestrict_aux _ z (fun j ↦ x ⟨j.1, not_not.mp j.2⟩) i c
