Theorems · Theorem · complex analysis

FormalMultilinearSeries.restrictScalars.congr_simp

∀ (𝕜 : Type u) {𝕜' : Type u'} {E : Type v} {F : Type w} [inst : Semiring 𝕜] [inst_1 : AddCommMonoid E]
  [inst_2 : Module 𝕜 E] [inst_3 : TopologicalSpace E] [inst_4 : ContinuousAdd E] [inst_5 : ContinuousConstSMul 𝕜 E]
  [inst_6 : AddCommMonoid F] [inst_7 : Module 𝕜 F] [inst_8 : TopologicalSpace F] [inst_9 : ContinuousAdd F]
  [inst_10 : ContinuousConstSMul 𝕜 F] [inst_11 : Semiring 𝕜'] [inst_12 : SMul 𝕜 𝕜'] [inst_13 : Module 𝕜' E]
  [inst_14 : ContinuousConstSMul 𝕜' E] [inst_15 : IsScalarTower 𝕜 𝕜' E] [inst_16 : Module 𝕜' F]
  [inst_17 : ContinuousConstSMul 𝕜' F] [inst_18 : IsScalarTower 𝕜 𝕜' F] (p p_1 : FormalMultilinearSeries 𝕜' E F),
  p = p_1 → ∀ (n : ℕ), FormalMultilinearSeries.restrictScalars 𝕜 p n = FormalMultilinearSeries.restrictScalars 𝕜 p_1 n

Defined in

Mathlib.Analysis.SpecialFunctions.Complex.Analytic

Cited by

0 results in Mathlib

Foundations

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

Assumes

SemiringAddCommMonoidModuleTopologicalSpaceContinuousAddContinuousConstSMulAddCommMonoidModuleTopologicalSpaceContinuousAddContinuousConstSMulSemiringSMulModuleContinuousConstSMulIsScalarTowerModuleContinuousConstSMulIsScalarTower