diff --git a/Mathlib/Algebra/BigOperators/Group/Finset/Basic.lean b/Mathlib/Algebra/BigOperators/Group/Finset/Basic.lean
index f0c05c6a1fa5f9..64433c610922ba 100644
--- a/Mathlib/Algebra/BigOperators/Group/Finset/Basic.lean
+++ b/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]