Revision #2122 → #3747 · back to history
1e0097d2c301b8506313ed5d1a01397336fbb45683d826fdc0e21fc7ab28| Field | From #2122 | To #3747 |
|---|---|---|
| kind | example | theorem |
| label | Dilogarithm of one via Basel problem | Basel problem |
| mathlib.match_kind | — | exact |
| note | Mathlib proves the Basel sum `hasSum_zeta_two : HasSum (1/n²) (π²/6)` but does not define the dilogarithm or this specific Fubini-derived identity. | The Basel identity ∑ 1/n² = π²/6 is `hasSum_zeta_two` in Mathlib. |
| status | partial | formalized |
522c98b0b7e8