Theorems · Theorem · functional analysis

TrivSqZeroExt.snd_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 →
    ∀ (n : ℕ),
      ((NormedSpace.expSeries 𝕜 (TrivSqZeroExt R M) (n + 1)) fun x_1 => x).snd =
        ((NormedSpace.expSeries 𝕜 R n) fun x_1 => x.fst) • x.snd

Defined in

Mathlib.Analysis.Normed.Algebra.TrivSqZeroExt

Cited by

1 results in Mathlib

Foundations

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

Assumes

FieldCharZeroRingAddCommGroupAlgebraModuleModuleModuleSMulCommClassIsScalarTowerIsScalarTowerTopologicalSpaceTopologicalSpaceIsTopologicalRingIsTopologicalAddGroupContinuousSMulContinuousSMul