primPart_mul — Mathlib

English

The primitive part of a product equals the product of the primitive parts, provided the product is nonzero: (p q).primPart = p.primPart q.primPart.

Русский

Примитивная часть произведения равна произведению примитивных частей при p q ≠ 0.

LaTeX

$$$(p q).primPart = p.primPart \cdot q.primPart$$$

Lean4

@[simp]
theorem primPart_mul {p q : R[X]} (h0 : p * q ≠ 0) : (p * q).primPart = p.primPart * q.primPart :=
  by
  rw [Ne, ← content_eq_zero_iff, ← C_eq_zero] at h0
  apply mul_left_cancel₀ h0
  conv_lhs => rw [← (p * q).eq_C_content_mul_primPart, p.eq_C_content_mul_primPart, q.eq_C_content_mul_primPart]
  rw [content_mul, RingHom.map_mul]
  ring

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