Theorems · Definition · commutative algebra

MvPowerSeries.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} →
                [IsTopologicalSemiring R] →
                  [IsUniformAddGroup R] →
                    [IsUniformAddGroup S] →
                      [CompleteSpace S] →
                        [T2Space S] →
                          [IsTopologicalRing S] →
                            [IsLinearTopology S S] →
                              [inst_11 : Algebra R S] →
                                [ContinuousSMul R S] → MvPowerSeries.HasEval a → MvPowerSeries σ R →ₐ[R] S

Evaluation of power series at adequate elements, as an AlgHom

Defined in

Mathlib.RingTheory.MvPowerSeries.Evaluation

Cited by

18 results in Mathlib

Foundations

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

Assumes

CommRingUniformSpaceCommRingUniformSpaceIsTopologicalSemiringIsUniformAddGroupIsUniformAddGroupCompleteSpaceT2SpaceIsTopologicalRingIsLinearTopologyAlgebraContinuousSMul