degreesLE_nsmul — Mathlib

English

Degrees bound under n-fold scaling corresponds to nth power of the bound.

Русский

Граница степеней при умножении на n соответствует n-ной степени границы.

LaTeX

$$$\\\\operatorname{degreesLE}(R,\\\\sigma, n \\cdot s) = (\\\\operatorname{degreesLE}(R,\\\\sigma, s))^n$$$

Lean4

theorem degreesLE_nsmul : ∀ n, degreesLE R σ (n • s) = degreesLE R σ s ^ n
  | 0 => by simp
  | k + 1 => by simp only [pow_succ, degreesLE_nsmul, degreesLE_add, add_smul, one_smul]

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