natDegree_mul_C_eq_of_mul_ne_zero

English

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

Русский

Если 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_mul_C_eq_of_mul_ne_zero`
force the polynomial `p` to be non-zero, via `p.leadingCoeff ≠ 0`.
-/
theorem natDegree_mul_C_eq_of_mul_ne_zero (h : p.leadingCoeff * a ≠ 0) : (p * C a).natDegree = p.natDegree :=
  by
  refine eq_natDegree_of_le_mem_support (natDegree_mul_C_le p a) ?_
  refine mem_support_iff.mpr ?_
  rwa [coeff_mul_C]

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