Theorems · Definition · functional analysis
LineDeriv.iteratedLineDerivOp
{V : Type u_11} → {E : Type u_12} → [LineDeriv V E E] → {n : ℕ} → (Fin n → V) → E → E∂^{m} f is the iterated line derivative of f, where m is a finite number of (different)
directions.
- Cited by
- 18 results in Mathlib
- Foundations
- Depth 25 from the axioms · uses propext
- Assumes
- LineDeriv
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites3
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Fin.tailproof · cited by 74
- LineDeriv.lineDerivOpproof · cited by 60
- LineDerivstatement and proof · cited by 29
Cited by19
Results whose statement or proof uses this declaration.
- LineDeriv.iteratedLineDerivOp_succ_leftstatement · cited by 4
- LineDeriv.iteratedLineDerivOp_addstatement and proof · cited by 3
- LineDeriv.iteratedLineDerivOpCLMproof · cited by 1
- Distribution.IsVanishingOn.iteratedLineDerivOpstatement and proof · cited by 1
- Distribution.TemperedDistribution.IsVanishingOn.iteratedLineDerivOpstatement and proof · cited by 1
- LineDeriv.continuous_iteratedLineDerivOpstatement and proof · cited by 0
- LineDeriv.iteratedLineDerivOpCLM_applystatement · cited by 0
- LineDeriv.iteratedLineDerivOp_const_eq_iter_lineDerivOpstatement and proof · cited by 0
- LineDeriv.iteratedLineDerivOp_fin_zerostatement · cited by 0
- LineDeriv.iteratedLineDerivOp_negstatement and proof · cited by 0
- LineDeriv.iteratedLineDerivOp_onestatement · cited by 0
- LineDeriv.iteratedLineDerivOp_smulstatement and proof · cited by 0