natDegree_smul_le_of_le

Mathlib.Tactic.ComputeDegree

URI: https://scilib.ai/kg/mathlib#Mathlib.Tactic.ComputeDegree.natDegree_smul_le_of_le

Lean4

theorem natDegree_smul_le_of_le (hf : natDegree f ≤ n) : natDegree (a • f) ≤ n :=
  (natDegree_smul_le a f).trans hf

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

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

Разделы

Аффилиация

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