Mathlib v3 is deprecated. Go to Mathlib v4

Theorem nnreal.summable_rpow_inv

Modification history

2021-10-14 16:25

src/analysis/p_series.lean

chore(analysis/p_series): add 2 more versions (#9703)

Added nnreal.summable_rpow_inv View on Github →