card_roots_le — Mathlib

English

The number of roots of a cubic is at most 3.

Русский

Количество корней кубического полинома не превосходит 3.

LaTeX

$$$$\\operatorname{card}(P.roots) \\le 3.$$$$

Lean4

theorem card_roots_le [IsDomain R] [DecidableEq R] : P.roots.toFinset.card ≤ 3 :=
  by
  apply (toFinset_card_le P.toPoly.roots).trans
  by_cases hP : P.toPoly = 0
  · exact (card_roots' P.toPoly).trans (by rw [hP, natDegree_zero]; exact zero_le 3)
  · exact WithBot.coe_le_coe.1 ((card_roots hP).trans degree_cubic_le)

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