Theorems · Theorem · commutative algebra

PowerSeries.HasEval.map

∀ {R : Type u_1} [inst : CommRing R] {S : Type u_2} [inst_1 : CommRing S] {φ : R →+* S} [inst_2 : TopologicalSpace R]
  [inst_3 : TopologicalSpace S], Continuous ⇑φ → ∀ {a : R}, PowerSeries.HasEval a → PowerSeries.HasEval (φ a)

[Bourbaki, Algebra, chap. 4, §4, n°3, Prop. 4 (i) (a & b)][bourbaki1981].

Defined in

Mathlib.RingTheory.PowerSeries.Evaluation

Cited by

3 results in Mathlib

Foundations

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

Assumes

CommRingCommRingTopologicalSpaceTopologicalSpace