English
The content of X multiplied by a polynomial p equals the content of p.
Русский
Содержимое X·p равно содержимому p.
LaTeX
$$$$ content(X \\cdot p) = content(p) $$$$
Lean4
theorem content_X_mul {p : R[X]} : content (X * p) = content p :=
by
rw [content, content, Finset.gcd_def, Finset.gcd_def]
refine congr rfl ?_
have h : (X * p).support = p.support.map ⟨Nat.succ, Nat.succ_injective⟩ :=
by
ext a
simp only [Finset.mem_map, Function.Embedding.coeFn_mk, Ne, mem_support_iff]
rcases a with - | a
· simp
rw [mul_comm, coeff_mul_X]
constructor
· intro h
use a
· rintro ⟨b, ⟨h1, h2⟩⟩
rw [← Nat.succ_injective h2]
apply h1
rw [h]
simp only [Finset.map_val, Function.comp_apply, Function.Embedding.coeFn_mk, Multiset.map_map]
refine congr (congr rfl ?_) rfl
ext a
rw [mul_comm]
simp [coeff_mul_X]
