English
If natDegree p = natDegree q, then r^{natDegree p - natDegree(p+q)} · (p+q).scaleRoots r = p.scaleRoots r + q.scaleRoots r.
Русский
Если natDegree p = natDegree q, то $r^{natDegree p - natDegree(p+q)} (p+q).scaleRoots r = p.scaleRoots r + q.scaleRoots r$.
LaTeX
$$$ r^{\operatorname{natDegree}(p) - \operatorname{natDegree}(p + q)} \cdot (p + q).\scaleRoots r = p.\scaleRoots r + q.\scaleRoots r $$$
Lean4
theorem add_scaleRoots_of_natDegree_eq (p q : R[X]) (r : R) (h : natDegree p = natDegree q) :
r ^ (natDegree p - natDegree (p + q)) • (p + q).scaleRoots r = p.scaleRoots r + q.scaleRoots r :=
by
ext n; simp only [coeff_smul, coeff_scaleRoots, coeff_add, smul_eq_mul, mul_comm (r ^ _), ← h, ← add_mul]
#adaptation_note /-- v4.7.0-rc1
Previously `mul_assoc` was part of the `simp only` above, and this `rw` was not needed.
but this now causes a max rec depth error. -/
rw [mul_assoc, ← pow_add]
cases lt_or_ge (natDegree (p + q)) n with
| inl hn => simp only [← coeff_add, coeff_eq_zero_of_natDegree_lt hn, zero_mul]
| inr hn => rw [add_comm (_ - n), tsub_add_tsub_cancel (natDegree_add_le_of_degree_le le_rfl h.ge) hn]
