deg_pow

Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization

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

English

Taking the n-th power scales degree by n: deg(c^n) = n · deg(c).

Русский

Степень n-го степенного множителя даёт deg(c^n) = n · deg(c).

LaTeX

$$$\\deg(c^n) = n \\cdot \\deg(c)$$$

Lean4

@[simp]
theorem deg_pow (c : NumDenSameDeg 𝒜 x) (n : ℕ) : (c ^ n).deg = n • c.deg :=
  rfl

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

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

Разделы

Аффилиация

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