mem_leadingCoeffNth_zero — Mathlib

English

The degree-zero leading coefficient membership corresponds exactly to C x ∈ I.

Русский

При n = 0 место принадлежности соответствует C x ∈ I.

LaTeX

$$$x \\in I.leadingCoeffNth 0 \\iff C x \\in I$$$

Lean4

theorem mem_leadingCoeffNth_zero (x) : x ∈ I.leadingCoeffNth 0 ↔ C x ∈ I :=
  (mem_leadingCoeffNth _ _ _).trans
    ⟨fun ⟨p, hpI, hpdeg, hpx⟩ => by
      rwa [← hpx, Polynomial.leadingCoeff, Nat.eq_zero_of_le_zero (natDegree_le_of_degree_le hpdeg), ←
        eq_C_of_degree_le_zero hpdeg],
      fun hx => ⟨C x, hx, degree_C_le, leadingCoeff_C x⟩⟩

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