English
Given finite s and φ, if k is below each (order of f i) then the kth coefficient of φ multiplied by ∏ (1 − f i) equals the kth coefficient of φ.
Русский
При конечном наборе s и φ, если k меньше каждого order(f_i), то коэффициент k от φ·∏(1−f_i) равен коэффициенту k от φ.
LaTeX
$$$\forall k \forall s \forall φ \forall f:\ lbrace s, φ, f \rbrace,\ (\forall i \in s,\uparrow k < (f i).order) \Rightarrow \operatorname{coeff}_k(\phi\cdot\prod_{i\in s}(1-f i)) = \operatorname{coeff}_k(\phi)$$$
Lean4
theorem coeff_mul_prod_one_sub_of_lt_order {R ι : Type*} [CommRing R] (k : ℕ) (s : Finset ι) (φ : R⟦X⟧) (f : ι → R⟦X⟧) :
(∀ i ∈ s, ↑k < (f i).order) → coeff k (φ * ∏ i ∈ s, (1 - f i)) = coeff k φ := by
classical
induction s using Finset.induction_on with
| empty => simp
| insert a s ha ih =>
intro t
simp only [Finset.mem_insert, forall_eq_or_imp] at t
rw [Finset.prod_insert ha, ← mul_assoc, mul_right_comm, coeff_mul_one_sub_of_lt_order _ t.1]
exact ih t.2
