coeff_mul_one_sub_of_lt_order — Mathlib

English

For a finite set s of indices and functions f_i, if k is below each f_i's order, the kth coefficient of φ multiplied by ∏(1−f_i) equals the kth coefficient of φ.

Русский

Для конечного множества индексов s и функций f_i, если k меньше каждого order(f_i), то коэффициент k от φ·∏(1−f_i) равен коэффициенту k у φ.

LaTeX

$$$\forall k,\forall s,\forall φ,\forall f:\, s.\to R\langle X \rangle,\ (\forall i\in s,\uparrow k < (\operatorname{order}(f i)))\Rightarrow \operatorname{coeff}_k\Big(\phi\cdot\prod_{i\in s}(1-f i)\Big) = \operatorname{coeff}_k(\phi)$$$

Lean4

theorem coeff_mul_one_sub_of_lt_order {R : Type*} [Ring R] {φ ψ : R⟦X⟧} (n : ℕ) (h : ↑n < ψ.order) :
    coeff n (φ * (1 - ψ)) = coeff n φ := by simp [coeff_mul_of_lt_order h, mul_sub]

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