eraseLead_support_card_lt

Mathlib.Algebra.Polynomial.EraseLead

URI: https://scilib.ai/kg/mathlib#Polynomial.eraseLead_support_card_lt

← MathLib Explorer

English

If f ≠ 0, then the cardinality of eraseLead f .support is strictly less than the cardinality of f .support.

Русский

Если f ≠ 0, то |eraseLead f| < |f| поддержка.

LaTeX

$$ #(eraseLead f).support < #f.support$$

Lean4

theorem eraseLead_support_card_lt (h : f ≠ 0) : #(eraseLead f).support < #f.support :=
  by
  rw [eraseLead_support]
  exact card_lt_card (erase_ssubset <| natDegree_mem_support_of_nonzero h)

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

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

Разделы

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

Аффилиация

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