card_roots_sub_C'

Mathlib.Algebra.Polynomial.Roots

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

← MathLib Explorer

English

For hp0 : 0 < deg p, Multiset.card (p − C a).roots ≤ natDegree p.

Русский

Для hp0 : 0 < deg p, Multiset.card (p − C a).roots ≤ natDegree p.

LaTeX

$$Multiset.card (p - C a).roots ≤ natDegree p.$$

Lean4

theorem card_roots_sub_C' {p : R[X]} {a : R} (hp0 : 0 < degree p) : Multiset.card (p - C a).roots ≤ natDegree p :=
  WithBot.coe_le_coe.1 (le_trans (card_roots_sub_C hp0) (le_of_eq <| degree_eq_natDegree fun h => by simp_all))

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

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

Разделы

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

Аффилиация

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