Theorems · Theorem · real analysis

HasFDerivAt.finset_prod

Deprecated since 2026-04-08Use HasFDerivAt.finsetProd instead.

∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {ι : Type u_5} {𝔸' : Type u_7} [inst_3 : NormedCommRing 𝔸'] [inst_4 : NormedAlgebra 𝕜 𝔸']
  {u : Finset ι} {g : ι → E → 𝔸'} {g' : ι → E →L[𝕜] 𝔸'} [inst_5 : DecidableEq ι] {x : E},
  (∀ i ∈ u, HasFDerivAt (g i) (g' i) x) →
    HasFDerivAt (fun x => ∏ i ∈ u, g i x) (∑ i ∈ u, (∏ j ∈ u.erase i, g j x) • g' i) x

Alias of HasFDerivAt.finsetProd.

Defined in

Mathlib.Analysis.Calculus.FDeriv.Mul

Cited by

0 results in Mathlib

Foundations

Depth 188 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NontriviallyNormedFieldNormedAddCommGroupNormedSpaceNormedCommRingNormedAlgebraDecidableEq