Theorems · Definition · commutative algebra

MvPowerSeries.IsRestricted

{R : Type u_1} → [NormedRing R] → {σ : Type u_2} → (σ → ℝ) → MvPowerSeries σ R → Prop

A multivariate powe0r series over a normed ring R is restricted for a tuple c if ‖coeff t f‖ * ∏ i ∈ t.support, c i ^ t i → 0 under the cofinite filter.

Defined in

Mathlib.RingTheory.MvPowerSeries.Restricted

Cited by

8 results in Mathlib

Foundations

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

Assumes

NormedRing