Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-10-14 16:25 393fe700

View on Github →

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

Estimated changes

Modified docs/undergrad.yaml

Modified src/analysis/p_series.lean

deleted theorem nnreal.summable_one_rpow_inv

added theorem nnreal.summable_rpow

added theorem nnreal.summable_rpow_inv

added theorem real.summable_nat_rpow