Theorems · Definition · commutative algebra

PowerSeries.aeval

{R : Type u_1} →
  [inst : CommRing R] →
    {S : Type u_2} →
      [inst_1 : CommRing S] →
        {a : S} →
          [inst_2 : UniformSpace R] →
            [inst_3 : UniformSpace S] →
              [IsUniformAddGroup R] →
                [IsTopologicalSemiring R] →
                  [IsUniformAddGroup S] →
                    [T2Space S] →
                      [CompleteSpace S] →
                        [IsTopologicalRing S] →
                          [IsLinearTopology S S] →
                            [inst_11 : Algebra R S] →
                              [ContinuousSMul R S] → PowerSeries.HasEval a → PowerSeries R →ₐ[R] S

For HasEval a, the evaluation homomorphism at a on PowerSeries, as an AlgHom.

Defined in

Mathlib.RingTheory.PowerSeries.Evaluation

Cited by

11 results in Mathlib

Foundations

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

Assumes

CommRingCommRingUniformSpaceUniformSpaceIsUniformAddGroupIsTopologicalSemiringIsUniformAddGroupT2SpaceCompleteSpaceIsTopologicalRingIsLinearTopologyAlgebraContinuousSMul