degree_normalize

Mathlib.Algebra.Polynomial.FieldDivision

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

English

For any p with coefficients in a field, degree of normalize p equals degree p.

Русский

Для любого p с коэффициентами в поле deg normalize p = deg p.

LaTeX

$$degree (normalize p) = degree p$$

Lean4

@[simp]
theorem degree_normalize [DecidableEq R] : degree (normalize p) = degree p := by simp [normalize_apply]

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

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

Разделы

Аффилиация

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