card_support_binomial — Mathlib

English

If k ≠ m and x, y ≠ 0, then the support has exactly two elements.

Русский

Если k ≠ m и x, y ≠ 0, то опора полинома содержит ровно два элемента.

LaTeX

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

Lean4

theorem card_support_binomial {k m : ℕ} (h : k ≠ m) {x y : R} (hx : x ≠ 0) (hy : y ≠ 0) :
    #(support (C x * X ^ k + C y * X ^ m)) = 2 := by
  rw [support_binomial h hx hy, card_insert_of_notMem (mt mem_singleton.mp h), card_singleton]

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