Theorems · Theorem · commutative algebra

MvPowerSeries.le_gaussNorm

∀ {R : Type u_1} {σ : Type u_2} (v : R → ℝ) (c : σ → ℝ) (f : MvPowerSeries σ R) [inst : Semiring R],
  MvPowerSeries.HasGaussNorm v c f →
    ∀ (t : σ →₀ ℕ), (v ((MvPowerSeries.coeff t) f) * t.prod fun x1 x2 => c x1 ^ x2) ≤ MvPowerSeries.gaussNorm v c f

Defined in

Mathlib.RingTheory.MvPowerSeries.GaussNorm

Cited by

5 results in Mathlib

Foundations

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

Assumes

Semiring