Theorems · Theorem · functional analysis
LineDeriv.lineDerivOp_left_sum
∀ {ι : Type u_1} {V : Type u_5} {E : Type u_6} {F : Type u_7} [inst : AddCommGroup V] [inst_1 : AddCommGroup E]
[inst_2 : AddCommGroup F] [inst_3 : LineDeriv V E F] [LineDerivAdd V E F] (f : ι → V) (x : E) (s : Finset ι),
LineDeriv.lineDerivOp (∑ i ∈ s, f i) x = ∑ i ∈ s, LineDeriv.lineDerivOp (f i) x- Cited by
- 0 results in Mathlib
- Foundations
- Depth 16 from the axioms · uses propext, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites9
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Finsetstatement and proof · cited by 13,712
- AddCommGroupstatement and proof · cited by 12,871
- Finset.sumstatement · cited by 5,195
- map_sumproof · cited by 455
- LineDeriv.lineDerivOpstatement and proof · cited by 60
- LineDerivstatement and proof · cited by 29
- AddMonoidHom.mk'proof · cited by 25
- LineDerivAddstatement and proof · cited by 19
- LineDerivAdd.lineDerivOp_left_addproof · cited by 3
Cited by0
Results whose statement or proof uses this declaration.
Nothing cites this yet.