Theorems · Theorem · functional analysis

TrivSqZeroExt.fst_expSeries

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

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

FieldRingAddCommGroupAlgebraModuleModuleModuleSMulCommClassIsScalarTowerIsScalarTowerTopologicalSpaceTopologicalSpaceIsTopologicalRingIsTopologicalAddGroupContinuousSMulContinuousSMul