Theorems · Theorem · functional analysis

TrivSqZeroExt.hasSum_expSeries_of_smul_comm

∀ (𝕜 : Type u_1) {R : Type u_3} {M : Type u_4} [inst : Field 𝕜] [CharZero 𝕜] [inst_2 : Ring R] [inst_3 : AddCommGroup M]
  [inst_4 : Algebra 𝕜 R] [inst_5 : Module 𝕜 M] [inst_6 : Module R M] [inst_7 : Module Rᵐᵒᵖ M]
  [inst_8 : SMulCommClass R Rᵐᵒᵖ M] [inst_9 : IsScalarTower 𝕜 R M] [inst_10 : IsScalarTower 𝕜 Rᵐᵒᵖ M]
  [inst_11 : TopologicalSpace R] [inst_12 : TopologicalSpace M] [inst_13 : IsTopologicalRing R]
  [inst_14 : IsTopologicalAddGroup M] [inst_15 : ContinuousSMul R M] [inst_16 : ContinuousSMul Rᵐᵒᵖ M]
  (x : TrivSqZeroExt R M),
  MulOpposite.op x.fst • x.snd = x.fst • x.snd →
    ∀ {e : R},
      HasSum (fun n => (NormedSpace.expSeries 𝕜 R n) fun x_1 => x.fst) e →
        HasSum (fun n => (NormedSpace.expSeries 𝕜 (TrivSqZeroExt R M) n) fun x_1 => x)
          (TrivSqZeroExt.inl e + TrivSqZeroExt.inr (e • x.snd))

If NormedSpace.exp R x.fst converges to e then NormedSpace.exp R x converges to inl e + inr (e • x.snd).

Defined in

Mathlib.Analysis.Normed.Algebra.TrivSqZeroExt

Cited by

1 results in Mathlib

Foundations

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

Assumes

FieldCharZeroRingAddCommGroupAlgebraModuleModuleModuleSMulCommClassIsScalarTowerIsScalarTowerTopologicalSpaceTopologicalSpaceIsTopologicalRingIsTopologicalAddGroupContinuousSMulContinuousSMul