{"count": 1, "header": "Found one declaration mentioning tsum and Real.sin.\n", "heartbeats": 1, "hits": [{"doc": null, "module": "Mathlib.Analysis.SpecialFunctions.Trigonometric.Series", "name": "Real.sin_eq_tsum", "type": " (r : \u211d) : Real.sin r = \u2211' (n : \u2115), (-1) ^ n * r ^ (2 * n + 1) / \u2191(2 * n + 1).factorial"}]}