Theorems · Theorem · commutative algebra

MvPowerSeries.aeval_eq_sum

∀ {σ : Type u_1} {R : Type u_2} [inst : CommRing R] [inst_1 : UniformSpace R] {S : Type u_3} [inst_2 : CommRing S]
  [inst_3 : UniformSpace S] {a : σ → S} [inst_4 : IsTopologicalSemiring R] [inst_5 : IsUniformAddGroup R]
  [inst_6 : IsUniformAddGroup S] [inst_7 : CompleteSpace S] [inst_8 : T2Space S] [inst_9 : IsTopologicalRing S]
  [inst_10 : IsLinearTopology S S] [inst_11 : Algebra R S] [inst_12 : ContinuousSMul R S] (ha : MvPowerSeries.HasEval a)
  (f : MvPowerSeries σ R),
  (MvPowerSeries.aeval ha) f = ∑' (d : σ →₀ ℕ), (MvPowerSeries.coeff d) f • d.prod fun s e => a s ^ e

Defined in

Mathlib.RingTheory.MvPowerSeries.Evaluation

Cited by

0 results in Mathlib

Foundations

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

Assumes

CommRingUniformSpaceCommRingUniformSpaceIsTopologicalSemiringIsUniformAddGroupIsUniformAddGroupCompleteSpaceT2SpaceIsTopologicalRingIsLinearTopologyAlgebraContinuousSMul