Project-declaredLean 4.32.0
Matrix Div add
Space.matrixDiv_add
Project documentation
The divergence of a matrix-valued spatial field. For a field T : Space d ā Matrix (Fin d) (Fin d) ā, matrixDiv T is the vector field whose ith component is ā j, ā[j] (fun x => T x i j) x. -/ noncomputable def matrixDiv (d : ā) (T : Space d ā Matrix (Fin d) (Fin d) ā) : Space d ā EuclideanSpace ā (Fin d) := fun x => WithLp.toLp 2 fun i => div (fun...
physicsquantum field theoryrelativity
Source project: Physlib
Person-level attribution pending.