mathlib

19e214e2 - feat(algebra/normed_space/basic,algebra/group_with_zero/power): real.(f)?pow_{even,bit0}_norm and field fpow lemmas (#6757)

feat(algebra/normed_space/basic,algebra/group_with_zero/power): real.(f)?pow_{even,bit0}_norm and field fpow lemmas (#6757) Simplifcation of `norm` when to an even numeral power. Additionally, add `fpow` lemmas to match `pow` lemmas, and change `fpow_nonneg_to_nonneg` to `fpow_nonneg` to match `pow` naming.