degBound_succ — Mathlib

English

For any k, D and n, degBound k D (n+1) equals degBound k D n times degBound k D n times D n, after normalization.

Русский

Для любых k, D и n, degBound k D (n+1) равно degBound k D n умноженное на degBound k D n и на D n.

LaTeX

$$degBound\\,k\\,D\\,(n+1) = degBound\\,k\\,D\\,n \\cdot degBound\\,k\\,D\\,n \\cdot D\\,n$$

Lean4

@[simp]
theorem degBound_succ (k : ℕ) (D : ℕ → ℕ) (n) :
    degBound k D (n + 1) = numBound k D (n + 1) ^ numBound k D (n + 1) * degBound k D n := by rw [degBound]

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