monic_X_sub_C — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem monic_X_sub_C {ι : Type*} (m : MonomialOrder ι) (i : ι) (r : R) : m.Monic (X i - C r) :=
  by
  rw [sub_eq_add_neg, ← map_neg]
  apply monic_X_add_C

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