ne_zero — Mathlib

English

If d(x) = 0, then the value at x of the factorized rational function F(x) = ∏ᶠ u, (· − u)^{d(u)} is nonzero.

Русский

Если d(x) = 0, то значение функции F(x) = ∏ᶠ u (x − u)^{d(u)} не равно нулю.

LaTeX

$$$ d(x) = 0 \Rightarrow \left( \prod^{\mathrm{fin}}_{u} (\cdot - u)^{d(u)} \right)(x) \neq 0 $$$

Lean4

/-- Factorized rational functions are non-zero wherever the exponent is zero.
-/
theorem ne_zero {d : 𝕜 → ℤ} {x : 𝕜} (h : d x = 0) : (∏ᶠ u, (· - u) ^ d u) x ≠ 0 :=
  by
  by_cases h₁ : (fun u ↦ (· - u) ^ d u).mulSupport.Finite
  · rw [finprod_eq_prod _ h₁, Finset.prod_apply, Finset.prod_ne_zero_iff]
    intro z hz
    simp only [Pi.pow_apply, ne_eq]
    by_cases h₂ : x = z <;> simp_all [zpow_ne_zero, sub_ne_zero]
  · simp [finprod_of_infinite_mulSupport h₁]

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