degree_mul_comm — Mathlib

English

For p monic and any q, the degrees satisfy deg(p q) = deg(q p).

Русский

Для p моноического и любого q верно deg(p q) = deg(q p).

LaTeX

$$$Monic(p) \Rightarrow \deg(p q) = \deg(q p) \quad \text{для всех } q$$

Lean4

theorem degree_mul_comm (hp : p.Monic) (q : R[X]) : (p * q).degree = (q * p).degree :=
  by
  by_cases h : q = 0
  · simp [h]
  rw [degree_mul', hp.degree_mul]
  · exact add_comm _ _
  · rwa [hp.leadingCoeff, one_mul, leadingCoeff_ne_zero]

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