content_C_mul — Mathlib

English

For any r and p, the content of C r times p equals normalize r times the content of p.

Русский

Для любого r и p содержимое C r · p равно normalize r · p.content.

LaTeX

$$$$ (C r \\cdot p).content = normalize(r) \\cdot p.content $$$$

Lean4

theorem content_C_mul (r : R) (p : R[X]) : (C r * p).content = normalize r * p.content :=
  by
  by_cases h0 : r = 0; · simp [h0]
  rw [content]; rw [content]; rw [← Finset.gcd_mul_left]
  refine congr (congr rfl ?_) ?_ <;> ext <;> simp [h0, mem_support_iff]

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