degree_X_sub_C — Mathlib

English

Let ι be a type, m a MonomialOrder on ι, i ∈ ι, and r ∈ R with [CommRing R]. Then deg_m(X_i − C r) = single i 1.

Русский

Пусть ι — множество индексов, m — монономный порядок на ι, i ∈ ι и r ∈ R; deg_m(X_i − C r) = single i 1.

LaTeX

$$$ m.degree (X_i - C r) = \operatorname{single}_i(1) $$$

Lean4

theorem degree_X_sub_C [Nontrivial R] {ι : Type*} (m : MonomialOrder ι) (i : ι) (r : R) :
    m.degree (X i - C r) = single i 1 := by rw [sub_eq_add_neg, ← map_neg, degree_X_add_C]

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