English
If R is a commutative ring with a gcd-monoid, then the polynomial ring R[X] carries a NormalizedGCDMonoid structure.
Русский
Если R — коммутативное кольцо с ГДМ-моноидом, то кольцо полиномов R[X] поддерживает структуру NormalizedGCDMonoid.
LaTeX
$$$R[X] \text{ is a NormalizedGCDMonoid}$$$
Lean4
noncomputable instance (priority := 100) normalizedGcdMonoid : NormalizedGCDMonoid R[X] :=
letI := Classical.decEq R
normalizedGCDMonoidOfExistsLCM fun p q =>
by
rcases exists_primitive_lcm_of_isPrimitive p.isPrimitive_primPart q.isPrimitive_primPart with ⟨r, rprim, hr⟩
refine ⟨C (lcm p.content q.content) * r, fun s => ?_⟩
by_cases hs : s = 0
· simp [hs]
by_cases hpq : C (lcm p.content q.content) = 0
· rw [C_eq_zero, lcm_eq_zero_iff, content_eq_zero_iff, content_eq_zero_iff] at hpq
rcases hpq with (hpq | hpq) <;> simp [hpq, hs]
iterate 3 rw [dvd_iff_content_dvd_content_and_primPart_dvd_primPart hs]
rw [content_mul, rprim.content_eq_one, mul_one, content_C, normalize_lcm, lcm_dvd_iff,
primPart_mul (mul_ne_zero hpq rprim.ne_zero), rprim.primPart_eq,
(isUnit_primPart_C (lcm p.content q.content)).mul_left_dvd, ← hr s.primPart]
tauto
