degree_C_mul_of_isUnit — Mathlib

English

If a is a unit in R, then for any p, deg(p * C(a)) = deg(p).

Русский

Если a является единицей в R, то для любого p deg(p · C(a)) = deg(p).

LaTeX

$$deg(p * C(a)) = deg(p) при IsUnit(a)$$

Lean4

theorem degree_C_mul_of_isUnit (ha : IsUnit a) (p : R[X]) : (C a * p).degree = p.degree :=
  by
  obtain rfl | hp := eq_or_ne p 0
  · simp
  nontriviality R
  rw [degree_mul', degree_C ha.ne_zero]
  · simp
  · simpa [ha.mul_right_eq_zero]

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