Theorems · Theorem · commutative algebra

PowerSeries.aeval_unique

∀ {R : Type u_1} [inst : CommRing R] {S : Type u_2} [inst_1 : CommRing S] [inst_2 : UniformSpace R]
  [inst_3 : UniformSpace S] [inst_4 : IsUniformAddGroup R] [inst_5 : IsTopologicalSemiring R]
  [inst_6 : IsUniformAddGroup S] [inst_7 : T2Space S] [inst_8 : CompleteSpace S] [inst_9 : IsTopologicalRing S]
  [inst_10 : IsLinearTopology S S] [inst_11 : Algebra R S] [inst_12 : ContinuousSMul R S] {ε : PowerSeries R →ₐ[R] S}
  (hε : Continuous ⇑ε), PowerSeries.aeval ⋯ = ε

Defined in

Mathlib.RingTheory.PowerSeries.Evaluation

Cited by

0 results in Mathlib

Foundations

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

Assumes

CommRingCommRingUniformSpaceUniformSpaceIsUniformAddGroupIsTopologicalSemiringIsUniformAddGroupT2SpaceCompleteSpaceIsTopologicalRingIsLinearTopologyAlgebraContinuousSMul