English
Let ι be a type, R a nontrivial ring, and m a MonomialOrder on ι. For i ∈ ι and r ∈ R, the degree of X_i + C r with respect to m is the singleton function that assigns 1 to i and 0 elsewhere, i.e. m.degree (X_i + C r) = single i 1.
Русский
Пусть ι — множество индексов, R — ненулевое кольцо, и m — монономный порядок на ι. Для i ∈ ι и r ∈ R deg_m(X_i + C r) совпадает с функцией single i 1, т.е. deg_m(X_i + C r) = single i 1.
LaTeX
$$$ m.degree (X_i + C r) = \operatorname{single}_i(1) $$$
Lean4
theorem degree_X_add_C [Nontrivial R] {ι : Type*} (m : MonomialOrder ι) (i : ι) (r : R) :
m.degree (X i + C r) = single i 1 := by
rw [degree_add_of_lt, degree_X]
simp only [degree_C, map_zero, degree_X]
rw [← bot_eq_zero, bot_lt_iff_ne_bot, bot_eq_zero, ← map_zero m.toSyn]
simp
