Theorems · Theorem · functional analysis

LineDeriv.tensorLineDerivTwo.congr_simp

∀ (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 f_1 : V₁),
  f = f_1 → LineDeriv.tensorLineDerivTwo R f = LineDeriv.tensorLineDerivTwo R f_1

Defined in

Mathlib.Analysis.Distribution.DerivNotation

Cited by

0 results in Mathlib

Foundations

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

Assumes

LineDerivLineDerivAddCommGroupAddCommGroupAddCommGroupCommRingAddCommGroupModuleModuleModuleLineDerivAddLineDerivAddLineDerivSMulLineDerivLeftSMulLineDerivLeftSMul