Add docstrings for reversed range telescoping lemmas (#39605)

This PR adds docstrings for two existing `Finset` telescoping lemmas and their additive versions generated by `to_additive`:

* `Finset.prod_range_div'` / `Finset.sum_range_sub'`
* `Finset.eq_prod_range_div` / `Finset.eq_sum_range_sub`

It is documentation-only: no declarations or imports are changed.

CI has passed.

AI assistance: Codex was used to help inspect the public PR/CI status and update this PR description.

Author: Qinghev

Mathlib/Algebra/BigOperators/Group/Finset/Basic.lean

@@ -896,11 +896,17 @@ additive group reduces to the difference of the last and first terms. -/]
 lemma prod_range_div (f : ℕ → G) (n : ℕ) : (∏ i ∈ range n, f (i + 1) / f i) = f n / f 0 := by
   apply prod_range_induction <;> simp
 
-@[to_additive]
+/-- A reversed telescoping product along `{0, ..., n - 1}` of a commutative-group-valued function
+reduces to the ratio of the first and last factors. -/
+@[to_additive /-- A reversed telescoping sum along `{0, ..., n - 1}` of a function valued in a
+commutative additive group reduces to the difference of the first and last terms. -/]
 lemma prod_range_div' (f : ℕ → G) (n : ℕ) : (∏ i ∈ range n, f i / f (i + 1)) = f 0 / f n := by
   apply prod_range_induction <;> simp
 
-@[to_additive]
+/-- Express `f n` as `f 0` multiplied by the telescoping product of consecutive ratios from
+`0` to `n - 1`. -/
+@[to_additive /-- Express `f n` as `f 0` plus the telescoping sum of consecutive differences from
+`0` to `n - 1`. -/]
 lemma eq_prod_range_div (f : ℕ → G) (n : ℕ) : f n = f 0 * ∏ i ∈ range n, f (i + 1) / f i := by
   rw [prod_range_div, mul_div_cancel]