natDegree_comp_eq_of_mul_ne_zero — Mathlib

English

If p and q are such that p.leadingCoeff · q.leadingCoeff^{p.natDegree} ≠ 0, then natDegree(p ∘ q) = natDegree(p) · natDegree(q).

Русский

Если p.leadingCoeff · q.leadingCoeff^{p.natDegree} ≠ 0, то natDegree(p ∘ q) = natDegree(p) · natDegree(q).

LaTeX

$$$\\operatorname{natDegree}(p \\circ q) = \\operatorname{natDegree}(p) \\cdot \\operatorname{natDegree}(q)$$$

Lean4

theorem natDegree_comp_eq_of_mul_ne_zero (h : p.leadingCoeff * q.leadingCoeff ^ p.natDegree ≠ 0) :
    natDegree (p.comp q) = natDegree p * natDegree q :=
  by
  by_cases hq : natDegree q = 0
  · exact le_antisymm natDegree_comp_le (by simp [hq])
  apply natDegree_eq_of_le_of_coeff_ne_zero natDegree_comp_le
  rwa [coeff_comp_degree_mul_degree hq]

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