mulSupport — Mathlib

English

The mulsupport of the factorized rational function equals the support of the exponent function d.

Русский

mulSupport факторизованной рациональной функции равен опоре функции экспоненты d.

LaTeX

$$$(fun u => (· - u) ^ d u).mulSupport = d.support$$$

Lean4

/-- Helper Lemma: Identify the support of `d` as the mulsupport of the product defining the factorized
rational function.
-/
theorem mulSupport (d : 𝕜 → ℤ) : (fun u ↦ (· - u) ^ d u).mulSupport = d.support :=
  by
  ext u
  constructor <;> intro h
  · simp_all only [mem_mulSupport, ne_eq, mem_support]
    by_contra hCon
    simp_all [zpow_zero]
  · simp_all only [mem_mulSupport, ne_eq, ne_iff]
    use u
    simp_all [zero_zpow_eq_one₀]

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