coeff_mul_right_one_sub_of_lt_weightedOrder

English

If a weight d is less than the weighted order of g, then coeff_d((1-g)*f) = coeff_d f.

Русский

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

LaTeX

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

Lean4

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

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