numBound_zero

Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity

URI: https://scilib.ai/kg/mathlib#ChevalleyThm.MvPolynomialC.numBound_zero

English

For any k and D, numBound k D 0 equals k.

Русский

Для любых k и D значение numBound k D (0) равно k.

LaTeX

$$numBound\\,k\\,D\\,0 = k$$

Lean4

@[simp]
theorem numBound_zero (k : ℕ) (D : ℕ → ℕ) : numBound k D 0 = k := by rw [numBound]

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

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

Разделы

Аффилиация

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