deg_add

Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization

URI: https://scilib.ai/kg/mathlib#HomogeneousLocalization.NumDenSameDeg.deg_add

English

The degree of the sum equals the sum of degrees: (p + q).deg = p.deg + q.deg.

Русский

Степень суммы равна сумме степеней: deg(p+q)=deg(p)+deg(q).

LaTeX

$$$\\deg(p+q) = \\deg(p) + \\deg(q)$$$

Lean4

@[simp]
theorem deg_add (c1 c2 : NumDenSameDeg 𝒜 x) : (c1 + c2).deg = c1.deg + c2.deg :=
  rfl

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

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

Разделы

Аффилиация

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