degree_C_mul_of_mul_ne_zero

Mathlib.Algebra.Polynomial.Degree.Lemmas

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

← MathLib Explorer

English

degree_C_mul_of_mul_ne_zero: If a · p.leadingCoeff ≠ 0, then degree(C a · p) = degree(p).

Русский

Если a · p.leadingCoeff ≠ 0, то degree(C a · p) = degree(p).

LaTeX

$$$a \\cdot p.leadingCoeff \\neq 0 \\Rightarrow \\deg(\\,C a \\cdot p\\,) = \\deg(p)$$$

Lean4

theorem degree_C_mul_of_mul_ne_zero (h : a * p.leadingCoeff ≠ 0) : (C a * p).degree = p.degree := by
  rw [degree_mul' (by simpa)]; simp [left_ne_zero_of_mul h]

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

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

Разделы

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

Аффилиация

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