content_C — Mathlib

English

For r in R and p in R[X], the content of C r times p equals normalize r times content p, provided r ≠ 0; if r = 0, both sides are zero.

Русский

Для r в R и p в R[X] содержимое C r·p равно normalize r·p.content; при r = 0 это нули.

LaTeX

$$$$ (C r \\cdot p).content = \\operatorname{normalize}(r) \\cdot p.\\text{content} $$$$

Lean4

@[simp]
theorem content_C {r : R} : (C r).content = normalize r :=
  by
  rw [content]
  by_cases h0 : r = 0
  · simp [h0]
  have h : (C r).support = {0} := support_monomial _ h0
  simp [h]

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