card_roots'

Mathlib.Algebra.Polynomial.Roots

URI: https://scilib.ai/kg/mathlib#Polynomial.card_roots'

← MathLib Explorer

English

The cardinality of p.roots is at most natDegree p.

Русский

Мощность p.roots не превосходит natDegree p.

LaTeX

$$Multiset.card p.roots ≤ natDegree p.$$

Lean4

theorem card_roots' (p : R[X]) : Multiset.card p.roots ≤ natDegree p :=
  by
  by_cases hp0 : p = 0
  · simp [hp0]
  exact WithBot.coe_le_coe.1 (le_trans (card_roots hp0) (le_of_eq <| degree_eq_natDegree hp0))

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru