natDegree_eq_one — Mathlib

English

natDegree(p) = 1 if and only if there exist a ≠ 0 and b with p = C a * X + C b.

Русский

natDegree(p) = 1 тогда и только тогда, когда существуют a ≠ 0 и b такие, что p = C a · X + C b.

LaTeX

$$$\operatorname{natDegree}(p) = 1 \iff \exists a \neq 0, \exists b, p = C a * X + C b$$$

Lean4

theorem natDegree_eq_one : p.natDegree = 1 ↔ ∃ a ≠ 0, ∃ b, C a * X + C b = p :=
  by
  refine ⟨fun hp ↦ ⟨p.coeff 1, fun h ↦ ?_, p.coeff 0, ?_⟩, ?_⟩
  · rw [← hp, coeff_natDegree, leadingCoeff_eq_zero] at h
    simp_all
  · ext n
    obtain _ | _ | n := n
    · simp
    · simp
    · simp only [coeff_add, coeff_mul_X, coeff_C_succ, add_zero]
      rw [coeff_eq_zero_of_natDegree_lt]
      simp [hp]
  · rintro ⟨a, ha, b, rfl⟩
    simp [ha]

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