natDegree_C_mul_of_mul_ne_zero — Mathlib

English

natDegree_C_mul_of_mul_ne_zero: If a · p.leadingCoeff ≠ 0, then natDegree(C a · p) = natDegree(p).

Русский

Если a · p.leadingCoeff ≠ 0, то natDegree(C a · p) = natDegree(p).

LaTeX

$$$a \\cdot p.leadingCoeff \\neq 0 \\Rightarrow \\operatorname{natDegree}(\\,C a \\cdot p\\,) = \\operatorname{natDegree}(p)$$$

Lean4

/-- Although not explicitly stated, the assumptions of lemma `natDegree_C_mul_of_mul_ne_zero`
force the polynomial `p` to be non-zero, via `p.leadingCoeff ≠ 0`.
-/
theorem natDegree_C_mul_of_mul_ne_zero (h : a * p.leadingCoeff ≠ 0) : (C a * p).natDegree = p.natDegree :=
  by
  refine eq_natDegree_of_le_mem_support (natDegree_C_mul_le a p) ?_
  refine mem_support_iff.mpr ?_
  rwa [coeff_C_mul]

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