degree_le_mul_left — Mathlib

English

If q ≠ 0 in R[X], then deg(p) ≤ deg(p q) for any p ∈ R[X].

Русский

Если q ≠ 0 в R[X], то deg(p) ≤ deg(p q) для любого p ∈ R[X].

LaTeX

$$$\deg(p) \le \deg(p q) \quad\text{for } q \neq 0.$$$

Lean4

theorem degree_le_mul_left (p : R[X]) (hq : q ≠ 0) : degree p ≤ degree (p * q) := by
  classical
  obtain rfl | hp := eq_or_ne p 0
  · simp
  · rw [degree_mul, degree_eq_natDegree hp, degree_eq_natDegree hq]
    exact WithBot.coe_le_coe.2 (Nat.le_add_right _ _)

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