Theorems · Theorem · functional analysis

LineDeriv.iteratedLineDerivOp_add

∀ {V : Type u_5} {E : Type u_6} [inst : LineDeriv V E E] {n : ℕ} (m : Fin n → V) [inst_1 : AddCommGroup V]
  [inst_2 : AddCommGroup E] [LineDerivAdd V E E] (x y : E),
  LineDeriv.iteratedLineDerivOp m (x + y) = LineDeriv.iteratedLineDerivOp m x + LineDeriv.iteratedLineDerivOp m y

Defined in: Mathlib.Analysis.Distribution.DerivNotation
Cited by: 3 results in Mathlib
Foundations: Depth 26 from the axioms · uses propext
Assumes: LineDeriv AddCommGroup AddCommGroup LineDerivAdd

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites7

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

AddCommGroupstatement and proof · cited by 12,871
Fin.tailproof · cited by 74
LineDeriv.lineDerivOpproof · cited by 60
LineDerivstatement and proof · cited by 29
LineDerivAddstatement and proof · cited by 19
LineDeriv.iteratedLineDerivOpstatement and proof · cited by 18
LineDerivAdd.lineDerivOp_addproof · cited by 4

Cited by4

Results whose statement or proof uses this declaration.

LineDeriv.iteratedLineDerivOpCLMproof · cited by 1
LineDeriv.iteratedLineDerivOp_sumproof · cited by 0
LineDeriv.iteratedLineDerivOp_zeroproof · cited by 0
LineDeriv.iteratedLineDerivOp_negproof · cited by 0