C_mul

Mathlib.RingTheory.MvPolynomial.Homogeneous

URI: https://scilib.ai/kg/mathlib#MvPolynomial.IsHomogeneous.C_mul

English

Multiplication by a scalar of a homogeneous polynomial preserves its degree.

Русский

Умножение на константу данного полинома сохраняет его степень.

LaTeX

$$(IsHomogeneous(\phi, m)) \Rightarrow IsHomogeneous(C r * \phi, m)$$

Lean4

theorem C_mul (hφ : φ.IsHomogeneous m) (r : R) : (C r * φ).IsHomogeneous m := by
  simpa only [zero_add] using (isHomogeneous_C _ _).mul hφ

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

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

Разделы

Аффилиация

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