Theorems · Theorem · commutative algebra

MvPowerSeries.coe_aeval

∀ {σ : 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), ⇑(MvPowerSeries.aeval ha) = MvPowerSeries.eval₂ (algebraMap R S) a

Defined in

Mathlib.RingTheory.MvPowerSeries.Evaluation

Cited by

9 results in Mathlib

Foundations

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

Assumes

CommRingUniformSpaceCommRingUniformSpaceIsTopologicalSemiringIsUniformAddGroupIsUniformAddGroupCompleteSpaceT2SpaceIsTopologicalRingIsLinearTopologyAlgebraContinuousSMul