card_support_trinomial — Mathlib

English

If k < m < n and x, y, z ≠ 0, then the support has exactly three elements.

Русский

Если k < m < n и x, y, z ≠ 0, то опора полинома состоит из трёх элементов.

LaTeX

$$$$\#\operatorname{Supp}(C x X^k + C y X^m + C z X^n) = 3$$$$

Lean4

theorem card_support_trinomial {k m n : ℕ} (hkm : k < m) (hmn : m < n) {x y z : R} (hx : x ≠ 0) (hy : y ≠ 0)
    (hz : z ≠ 0) : #(support (C x * X ^ k + C y * X ^ m + C z * X ^ n)) = 3 := by
  rw [support_trinomial hkm hmn hx hy hz,
    card_insert_of_notMem (mt mem_insert.mp (not_or_intro hkm.ne (mt mem_singleton.mp (hkm.trans hmn).ne))),
    card_insert_of_notMem (mt mem_singleton.mp hmn.ne), card_singleton]

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