degree_eq_degree_of_associated — Mathlib

English

If two polynomials p and q are associated (differ by a unit factor), then their degrees are equal.

Русский

Если два многочлена p и q ассоциированы (отличаются на множитель-единицу), то их степени равны.

LaTeX

$$$$ \\deg(p) = \\deg(q) \\quad\\text{whenever } p \\sim q. $$$$

Lean4

theorem degree_eq_degree_of_associated (h : Associated p q) : degree p = degree q :=
  by
  let ⟨u, hu⟩ := h
  simp [hu.symm]

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