Theorems · Inductive type · commutative algebra

MvPowerSeries.HasEval

{σ : Type u_1} → {S : Type u_3} → [CommRing S] → [TopologicalSpace S] → (σ → S) → Prop

Families at which power series can be consistently evaluated

Defined in

Mathlib.RingTheory.MvPowerSeries.Evaluation

Cited by

37 results in Mathlib

Foundations

Depth 1 from the axioms · uses no axioms

Assumes

CommRingTopologicalSpace