cauchyBound_smul — Mathlib

English

For x ≠ 0, cauchyBound(x · p) = cauchyBound(p).

Русский

Для x ≠ 0, cauchyBound(x · p) = cauchyBound(p).

LaTeX

$$$$\cauchyBound\bigl(x \cdot p\bigr) = \cauchyBound(p)$$$$

Lean4

@[simp]
theorem cauchyBound_smul {x : K} (hx : x ≠ 0) (p : K[X]) : cauchyBound (x • p) = cauchyBound p :=
  by
  simp only [cauchyBound, (isRegular_of_ne_zero hx).left.isSMulRegular, natDegree_smul_of_smul_regular, coeff_smul,
    smul_eq_mul, nnnorm_mul, ← mul_finset_sup, leadingCoeff_smul_of_smul_regular, add_left_inj]
  apply mul_div_mul_left
  simpa

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