gaussNorm_eq_zero_iff — Mathlib

English

Under suitable hypotheses on v and the order of c, gaussNorm(v,c,p) = 0 iff p = 0.

Русский

При допустимых условиях на v и порядок c, gaussNorm(v,c,p) = 0 тогда и только тогда p = 0.

LaTeX

$$gaussNorm(v,c,p) = 0 \\Leftrightarrow p = 0$$

Lean4

@[simp]
theorem gaussNorm_eq_zero_iff [ZeroHomClass F R ℝ] [NonnegHomClass F R ℝ] (h_eq_zero : ∀ x : R, v x = 0 → x = 0)
    (hc : 0 < c) : p.gaussNorm v c = 0 ↔ p = 0 := by
  rw [← gaussNorm_coe_powerSeries _ _ (le_of_lt hc),
    PowerSeries.gaussNorm_eq_zero_iff h_eq_zero hc (by simpa only [coeff_coe] using aux_bdd v p), coe_eq_zero_iff]

Похожие утверждения