Theorems · Definition · functional analysis
LineDeriv.lineDerivOp
{V : Type u} → {E : Type v} → {F : outParam (Type w)} → [self : LineDeriv V E F] → V → E → F∂_{v} f is the line derivative of f in direction v. The meaning of this notation is
type-dependent.
- Cited by
- 60 results in Mathlib
- Foundations
- Depth 2 from the axioms · uses no axioms
- Assumes
- LineDeriv
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites1
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- LineDerivstatement and proof · cited by 29
Cited by71
Results whose statement or proof uses this declaration.
- LineDeriv.iteratedLineDerivOpproof · cited by 18
- LineDeriv.lineDerivOpCLMproof · cited by 9
- SchwartzMap.laplacian_eq_sumstatement · cited by 5
- LineDeriv.iteratedLineDerivOp_succ_leftstatement · cited by 4
- LineDerivAdd.lineDerivOp_addstatement · cited by 4
- SchwartzMap.integral_bilinear_lineDerivOp_right_eq_neg_leftstatement and proof · cited by 4
- LineDeriv.iteratedLineDerivOp_addproof · cited by 3
- LineDerivAdd.lineDerivOp_left_addstatement · cited by 3
- SchwartzMap.fourier_lineDerivOp_eqstatement · cited by 3
- SchwartzMap.integral_bilinear_laplacian_right_eq_leftproof · cited by 3
- TemperedDistribution.laplacian_eq_sumstatement · cited by 2
- SchwartzMap.lineDerivOp_fourier_eqstatement · cited by 2