Theorems · Theorem · global analysis

ContinuousMultilinearMap.toFormalMultilinearSeries.congr_simp

∀ {𝕜 : Type u} {F : Type w} [inst : Semiring 𝕜] [inst_1 : AddCommMonoid F] [inst_2 : Module 𝕜 F]
  [inst_3 : TopologicalSpace F] [inst_4 : ContinuousAdd F] [inst_5 : ContinuousConstSMul 𝕜 F] {ι : Type u_1}
  {E : ι → Type u_2} [inst_6 : (i : ι) → AddCommGroup (E i)] [inst_7 : (i : ι) → Module 𝕜 (E i)]
  [inst_8 : (i : ι) → TopologicalSpace (E i)] [inst_9 : ∀ (i : ι), IsTopologicalAddGroup (E i)]
  [inst_10 : ∀ (i : ι), ContinuousConstSMul 𝕜 (E i)] [inst_11 : Fintype ι] (f f_1 : ContinuousMultilinearMap 𝕜 E F),
  f = f_1 → ∀ (n : ℕ), f.toFormalMultilinearSeries n = f_1.toFormalMultilinearSeries n

Defined in

Mathlib.Analysis.Calculus.FDeriv.Analytic

Cited by

0 results in Mathlib

Foundations

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

Assumes

SemiringAddCommMonoidModuleTopologicalSpaceContinuousAddContinuousConstSMulAddCommGroupModuleTopologicalSpaceIsTopologicalAddGroupContinuousConstSMulFintype