degree_coe_units

Mathlib.Algebra.Polynomial.Degree.Units

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

English

For a unit u in the polynomial ring, degree(u) = 0.

Русский

Для единицы u в кольце многочленов, degree(u) = 0.

LaTeX

$$$ degree(u) = 0 $$$

Lean4

@[simp]
theorem degree_coe_units [Nontrivial R] (u : R[X]ˣ) : degree (u : R[X]) = 0 :=
  degree_eq_zero_of_isUnit ⟨u, rfl⟩

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

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

Разделы

Аффилиация

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