card_support_eq_one — Mathlib

English

The support has size one exactly when the polynomial is a single monomial with a nonzero coefficient: #f.support = 1 iff f = C x X^k with x ≠ 0.

Русский

Опора имеет размер единица тогда и только тогда, когда полином есть один моном с ненулевым коэффициентом: #f.support = 1 ⇔ f = C x X^k и x ≠ 0.

LaTeX

$$$#f.support = 1 \\iff \\exists k\\,\\exists x\\, (x \\neq 0) \\land f = C x \\cdot X^k$$$

Lean4

theorem card_support_eq_one : #f.support = 1 ↔ ∃ (k : ℕ) (x : R) (_ : x ≠ 0), f = C x * X ^ k :=
  by
  refine ⟨fun h => ?_, ?_⟩
  · obtain ⟨k, x, _, hx, rfl⟩ := card_support_eq.mp h
    exact ⟨k 0, x 0, hx 0, Fin.sum_univ_one _⟩
  · rintro ⟨k, x, hx, rfl⟩
    rw [support_C_mul_X_pow k hx, card_singleton]

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