degree_C_le

Mathlib.Algebra.Polynomial.Degree.Definitions

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

English

For any a, deg(C(a)) ≤ 0.

Русский

Для любого a выполняется deg(C(a)) ≤ 0.

LaTeX

$$degree(C(a)) \\le 0$$

Lean4

theorem degree_C_le : degree (C a) ≤ 0 := by
  by_cases h : a = 0
  · rw [h, C_0]
    exact bot_le
  · rw [degree_C h]

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

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

Разделы

Аффилиация

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