Structures · Analysis
LineDerivSMul
The line derivative commutes with scalar multiplication, ∂_{v} (r • x) = r • ∂_{v} x for all
r : R and x : E.
- Shape
- 4 explicit arguments · adds lineDerivOp_smul
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances2
- Real
- Complex
How is a type an instance?
Loading the hierarchy index…
Assumed by14
- LineDeriv.lineDerivOpCLM
- LineDeriv.tensorLineDerivTwo
- LineDeriv.laplacianCLM
- LineDeriv.laplacianCLM_eq_sum
- LineDeriv.iteratedLineDerivOpCLM
- LineDerivSMul.lineDerivOp_smul
- LineDeriv.tensorLineDerivTwo_eq_lineDerivOp_lineDerivOp
- LineDeriv.iteratedLineDerivOp_smul
- LineDeriv.tensorLineDerivTwo_canonicalCovariantTensor_eq_sum
- LineDeriv.bilinearLineDerivTwo
- LineDeriv.lineDerivOpCLM.congr_simp
- LineDeriv.lineDerivOpCLM_apply
- LineDeriv.iteratedLineDerivOpCLM_apply
- LineDeriv.tensorLineDerivTwo.congr_simp
Ancestors0
No ancestors.