exists_eq_gaussNorm — Mathlib

English

For any polynomial p, there exists an index i such that gaussNorm(v,c,p) equals v(coeff i) · c^i.

Русский

Для любого p существует индекс i такой, что gaussNorm(v,c,p) равно v(coeff i) · c^i.

LaTeX

$$∃ i, gaussNorm(v,c;p) = v(p.coeff i) · c^i$$

Lean4

theorem exists_eq_gaussNorm [ZeroHomClass F R ℝ] : ∃ i, p.gaussNorm v c = v (p.coeff i) * c ^ i :=
  by
  by_cases h_supp : p.support.Nonempty
  · simp only [gaussNorm, h_supp]
    obtain ⟨i, hi1, hi2⟩ := Finset.exists_mem_eq_sup' h_supp fun i ↦ (v (p.coeff i) * c ^ i)
    exact ⟨i, hi2⟩
  · simp_all

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