degreeOf_mul_X_of_ne — Mathlib

English

If i ≠ j, degreeOf i (f · X_j) equals degreeOf i f.

Русский

Если i ≠ j, deg_i(f X_j) = deg_i f.

LaTeX

$$$i \neq j \Rightarrow \deg_i(f X_j) = \deg_i f$$$

Lean4

theorem degreeOf_mul_X_of_ne {i j : σ} (f : MvPolynomial σ R) (h : i ≠ j) : degreeOf i (f * X j) = degreeOf i f := by
  classical
  simp only [degreeOf_eq_sup i, support_mul_X, Finset.sup_map]
  congr
  ext
  simp only [Finsupp.single, add_eq_left, addRightEmbedding_apply, coe_mk, Pi.add_apply, comp_apply, Finsupp.coe_add,
    Pi.single_eq_of_ne h]

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