Theorems · Theorem · commutative algebra

PowerSeries.gaussNorm_add_le_max

∀ {R : Type u_1} [inst : Semiring R] (v : R → ℝ) (c : ℝ) (f g : PowerSeries R),
  0 ≤ c →
    (∀ (a : R), v a ≥ 0) →
      (∀ (x y : R), v (x + y) ≤ max (v x) (v y)) →
        PowerSeries.HasGaussNorm v c f →
          PowerSeries.HasGaussNorm v c g →
            PowerSeries.gaussNorm v c (f + g) ≤ max (PowerSeries.gaussNorm v c f) (PowerSeries.gaussNorm v c g)

Defined in: Mathlib.RingTheory.PowerSeries.GaussNorm
Cited by: 0 results in Mathlib
Foundations: Depth 120 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: Semiring

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites7

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Realstatement and proof · cited by 25,697
Semiringstatement and proof · cited by 13,802
PowerSeriesstatement and proof · cited by 797
PowerSeries.gaussNormstatement · cited by 11
PowerSeries.HasGaussNormstatement and proof · cited by 5
PowerSeries.HasGaussNorm.hasMvGaussNormproof · cited by 3
MvPowerSeries.gaussNorm_add_le_maxproof · cited by 1

Cited by0

Results whose statement or proof uses this declaration.

Nothing cites this yet.