Theorems · Definition · functional analysis

LineDeriv.tensorLineDerivTwo

(R : Type u_4) →
  {E : Type u_6} →
    {V₁ : Type u_8} →
      {V₂ : Type u_9} →
        {V₃ : Type u_10} →
          [inst : LineDeriv E V₁ V₂] →
            [inst_1 : LineDeriv E V₂ V₃] →
              [inst_2 : AddCommGroup V₁] →
                [inst_3 : AddCommGroup V₂] →
                  [inst_4 : AddCommGroup V₃] →
                    [inst_5 : CommRing R] →
                      [inst_6 : AddCommGroup E] →
                        [inst_7 : Module R E] →
                          [inst_8 : Module R V₂] →
                            [inst_9 : Module R V₃] →
                              [LineDerivAdd E V₂ V₃] →
                                [LineDerivAdd E V₁ V₂] →
                                  [LineDerivSMul R E V₂ V₃] →
                                    [LineDerivLeftSMul R E V₁ V₂] →
                                      [LineDerivLeftSMul R E V₂ V₃] → V₁ → TensorProduct R E E →ₗ[R] V₃

The second derivative in terms lineDerivOp as a linear map from the tensor product. Mainly used to give an abstract definition of the Laplacian.

Defined in

Mathlib.Analysis.Distribution.DerivNotation

Cited by

4 results in Mathlib

Foundations

Depth 57 from the axioms · uses propext, Quot.sound

Assumes

LineDerivLineDerivAddCommGroupAddCommGroupAddCommGroupCommRingAddCommGroupModuleModuleModuleLineDerivAddLineDerivAddLineDerivSMulLineDerivLeftSMulLineDerivLeftSMul