coeff_mul_left_one_sub_of_lt_order

English

If the degree of d is less than the order of g, then the coefficient of d in f*(1-g) equals the coefficient of d in f.

Русский

Если deg(d) < ord(g), то коэффициент d в f*(1-g) равен коэффициенту d в f.

LaTeX

$$$ \deg(d) < \operatorname{ord}(g) \Rightarrow \operatorname{coeff}_d\left(f\cdot(1-g)\right) = \operatorname{coeff}_d f $$$

Lean4

theorem coeff_mul_left_one_sub_of_lt_order (d : σ →₀ ℕ) (h : degree d < g.order) : coeff d (f * (1 - g)) = coeff d f :=
  by
  rw [degree_eq_weight_one] at h
  exact coeff_mul_left_one_sub_of_lt_weightedOrder _ h

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