Theorems · Theorem · commutative algebra

MvPowerSeries.gaussNorm_eq_zero_iff

∀ {R : Type u_1} {σ : Type u_2} (v : R → ℝ) (c : σ → ℝ) (f : MvPowerSeries σ R) [inst : Semiring R],
  v 0 = 0 →
    (∀ (a : R), v a ≥ 0) →
      (∀ (x : R), v x = 0 → x = 0) →
        (∀ (i : σ), 0 < c i) → MvPowerSeries.HasGaussNorm v c f → (MvPowerSeries.gaussNorm v c f = 0 ↔ f = 0)

Defined in

Mathlib.RingTheory.MvPowerSeries.GaussNorm

Cited by

2 results in Mathlib

Foundations

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

Assumes

Semiring