coeff_mul_left_one_sub_of_lt_weightedOrder

English

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

Русский

Если weight w d < weightedOrder w g, то coeff_d(f(1-g)) = coeff_d(f).

LaTeX

$$coeff d (f * (1 - g)) = coeff d f if weight w d < g.weightedOrder w$$

Lean4

theorem coeff_mul_left_one_sub_of_lt_weightedOrder {d : σ →₀ ℕ} (h : (weight w d) < g.weightedOrder w) :
    coeff d (f * (1 - g)) = coeff d f :=
  by
  simp only [mul_sub, mul_one, map_sub, sub_eq_self]
  apply coeff_eq_zero_of_lt_weightedOrder w
  exact lt_of_lt_of_le (lt_of_lt_of_le h le_add_self) (le_weightedOrder_mul w)

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