monic_X_add_C — Mathlib

English

For any nontrivial ring R and any i ∈ ι, r ∈ R, the polynomial X_i + C r is monic with respect to the monomial order m.

Русский

Пусть R ненулевое кольцо; для любого i ∈ ι и r ∈ R ступенчатый полином X_i + C r является моническим по отношению к порядку мономов m.

LaTeX

$$$ m.Monic (X_i + C r) $$$

Lean4

theorem monic_X_add_C {ι : Type*} (m : MonomialOrder ι) (i : ι) (r : R) : m.Monic (X i + C r) :=
  by
  nontriviality R
  apply monic_X.add_of_lt
  simp [degree_C, degree_X, ← not_le, ← eq_zero_iff]

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