natDegree_mul' — Mathlib

English

Same as natDegree_mul' but stated explicitly; natDegree(p q) = natDegree p + natDegree q given lc(p) lc(q) ≠ 0.

Русский

То же, что и natDegree_mul', тождество natDegree(p q) = natDegree p + natDegree q при lc(p) lc(q) ≠ 0.

LaTeX

$$natDegree(p * q) = natDegree(p) + natDegree(q) при leadingCoeff p * leadingCoeff q ≠ 0$$

Lean4

theorem natDegree_mul' (h : leadingCoeff p * leadingCoeff q ≠ 0) : natDegree (p * q) = natDegree p + natDegree q :=
  have hp : p ≠ 0 := mt leadingCoeff_eq_zero.2 fun h₁ => h <| by rw [h₁, zero_mul]
  have hq : q ≠ 0 := mt leadingCoeff_eq_zero.2 fun h₁ => h <| by rw [h₁, mul_zero]
  natDegree_eq_of_degree_eq_some <| by rw [degree_mul' h, Nat.cast_add, degree_eq_natDegree hp, degree_eq_natDegree hq]

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