Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-05-12 16:23 0509c9c6

View on Github →

fix(analysis/special_functions/pow): fix norm_num extension (#14099) As reported on Zulip.

Estimated changes

modified theorem norm_num.rpow_pos