Theorems · Theorem · global analysis

fderivWithin_restrictScalars_comp

∀ {𝕜 : Type u_1} {𝕜' : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NontriviallyNormedField 𝕜']
  [inst_2 : NormedAlgebra 𝕜 𝕜'] {E : Type u_3} [inst_3 : NormedAddCommGroup E] [inst_4 : NormedSpace 𝕜 E]
  [inst_5 : NormedSpace 𝕜' E] [inst_6 : IsScalarTower 𝕜 𝕜' E] {F : Type u_4} [inst_7 : NormedAddCommGroup F]
  [inst_8 : NormedSpace 𝕜 F] [inst_9 : NormedSpace 𝕜' F] [inst_10 : IsScalarTower 𝕜 𝕜' F] {x : E} {n : ℕ} {s : Set E}
  {φ : E → E [×n]→L[𝕜'] F},
  DifferentiableWithinAt 𝕜' φ s x →
    UniqueDiffWithinAt 𝕜 s x →
      ⇑(fderivWithin 𝕜 (ContinuousMultilinearMap.restrictScalars 𝕜 ∘ φ) s x) =
        ContinuousMultilinearMap.restrictScalars 𝕜 ∘ ⇑(ContinuousLinearMap.restrictScalars 𝕜 (fderivWithin 𝕜' φ s x))

Derivation rule for compositions of scalar restriction with continuous multilinear maps.

Defined in

Mathlib.Analysis.Calculus.ContDiff.RestrictScalars

Cited by

1 results in Mathlib

Foundations

Depth 172 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NontriviallyNormedFieldNontriviallyNormedFieldNormedAlgebraNormedAddCommGroupNormedSpaceNormedSpaceIsScalarTowerNormedAddCommGroupNormedSpaceNormedSpaceIsScalarTower