isMonicOfDegree_one_iff — Mathlib

English

There is a characterization: IsMonicOfDegree p 1 iff there exists r with p = X + C r.

Русский

Существует характеристика: IsMonicOfDegree(p,1) эквивалентно существованию r such that p = X + C r.

LaTeX

$$$IsMonicOfDegree(p, 1) \\iff \\exists r, p = X + C r$$$

Lean4

theorem isMonicOfDegree_one_iff {f : R[X]} : IsMonicOfDegree f 1 ↔ ∃ r : R, f = X + C r :=
  by
  refine ⟨fun H ↦ ?_, fun ⟨r, H⟩ ↦ H ▸ isMonicOfDegree_X_add_one r⟩
  refine ⟨f.coeff 0, ?_⟩
  ext1 n
  rcases n.eq_zero_or_pos with rfl | hn
  · simp
  · exact H.coeff_eq (isMonicOfDegree_X_add_one _) (by cutsat)

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