Lean4
@[simp]
theorem content_mul {p q : R[X]} : (p * q).content = p.content * q.content := by
classical
suffices h : ∀ (n : ℕ) (p q : R[X]), (p * q).degree < n → (p * q).content = p.content * q.content
by
apply h
apply lt_of_le_of_lt degree_le_natDegree (WithBot.coe_lt_coe.2 (Nat.lt_succ_self _))
intro n p q hpq
induction n generalizing p q with
| zero =>
rw [Nat.cast_zero, Nat.WithBot.lt_zero_iff, degree_eq_bot, mul_eq_zero] at hpq
rcases hpq with (rfl | rfl) <;> simp
| succ n ih => ?_
by_cases p0 : p = 0
· simp [p0]
by_cases q0 : q = 0
· simp [q0]
rw [degree_eq_natDegree (mul_ne_zero p0 q0), Nat.cast_lt, Nat.lt_succ_iff_lt_or_eq, ← Nat.cast_lt (α := WithBot ℕ), ←
degree_eq_natDegree (mul_ne_zero p0 q0), natDegree_mul p0 q0] at hpq
rcases hpq with (hlt | heq)
· apply ih _ _ hlt
rw [← p.natDegree_primPart, ← q.natDegree_primPart, ← Nat.cast_inj (R := WithBot ℕ), Nat.cast_add, ←
degree_eq_natDegree p.primPart_ne_zero, ← degree_eq_natDegree q.primPart_ne_zero] at heq
rw [p.eq_C_content_mul_primPart, q.eq_C_content_mul_primPart]
suffices h : (q.primPart * p.primPart).content = 1 by
rw [mul_assoc, content_C_mul, content_C_mul, mul_comm p.primPart, mul_assoc, content_C_mul, content_C_mul, h,
mul_one, content_primPart, content_primPart, mul_one, mul_one]
rw [← normalize_content, normalize_eq_one, isUnit_iff_dvd_one, content_eq_gcd_leadingCoeff_content_eraseLead,
leadingCoeff_mul, gcd_comm]
apply (gcd_mul_dvd_mul_gcd _ _ _).trans
rw [content_mul_aux, ih, content_primPart, mul_one, gcd_comm, ← content_eq_gcd_leadingCoeff_content_eraseLead,
content_primPart, one_mul, mul_comm q.primPart, content_mul_aux, ih, content_primPart, mul_one, gcd_comm, ←
content_eq_gcd_leadingCoeff_content_eraseLead, content_primPart]
· rw [← heq, degree_mul, WithBot.add_lt_add_iff_right]
· apply degree_erase_lt p.primPart_ne_zero
· rw [Ne, degree_eq_bot]
apply q.primPart_ne_zero
· rw [mul_comm, ← heq, degree_mul, WithBot.add_lt_add_iff_left]
· apply degree_erase_lt q.primPart_ne_zero
· rw [Ne, degree_eq_bot]
apply p.primPart_ne_zero
