degree_mul_C_of_isUnit

Mathlib.Algebra.Polynomial.Degree.Operations

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

← MathLib Explorer

English

Same as above: deg(p * C(a)) = deg(p) when a is a unit.

Русский

То же: deg(p · C(a)) = deg(p) при a единица.

LaTeX

$$deg(p * C(a)) = deg(p) при IsUnit(a)$$

Lean4

theorem degree_mul_C_of_isUnit (ha : IsUnit a) (p : R[X]) : (p * C a).degree = p.degree :=
  by
  obtain rfl | hp := eq_or_ne p 0
  · simp
  nontriviality R
  rw [degree_mul', degree_C ha.ne_zero]
  · simp
  · simpa [ha.mul_left_eq_zero]

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

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

Разделы

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

Аффилиация

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