Theorems · Theorem · functional analysis

LineDeriv.tensorLineDerivTwo_eq_lineDerivOp_lineDerivOp

∀ {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₃]
  [inst_10 : LineDerivAdd E V₂ V₃] [inst_11 : LineDerivAdd E V₁ V₂] [inst_12 : LineDerivSMul R E V₂ V₃]
  [inst_13 : LineDerivLeftSMul R E V₁ V₂] [inst_14 : LineDerivLeftSMul R E V₂ V₃] (f : V₁) (v w : E),
  (LineDeriv.tensorLineDerivTwo R f) (v ⊗ₜ[R] w) = LineDeriv.lineDerivOp v (LineDeriv.lineDerivOp w f)

Defined in

Mathlib.Analysis.Distribution.DerivNotation

Cited by

1 results in Mathlib

Foundations

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

Assumes

LineDerivLineDerivAddCommGroupAddCommGroupAddCommGroupCommRingAddCommGroupModuleModuleModuleLineDerivAddLineDerivAddLineDerivSMulLineDerivLeftSMulLineDerivLeftSMul