Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-03-24 23:20 19e214e2

View on Github →

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.

Estimated changes

added theorem abs_fpow_bit0
added theorem abs_fpow_even
added theorem fpow_bit0_abs
added theorem fpow_bit0_neg
added theorem fpow_bit0_nonneg
added theorem fpow_bit0_pos
added theorem fpow_bit1_neg
added theorem fpow_bit1_neg_iff
added theorem fpow_bit1_nonneg_iff
added theorem fpow_bit1_nonpos_iff
added theorem fpow_bit1_pos_iff
added theorem fpow_eq_zero_iff
added theorem fpow_even_abs
added theorem fpow_even_neg
added theorem fpow_even_nonneg
added theorem fpow_even_pos
added theorem fpow_nonneg
deleted theorem fpow_nonneg_of_nonneg
added theorem fpow_odd_neg
added theorem fpow_odd_nonneg
added theorem fpow_odd_nonpos
added theorem fpow_odd_pos
added theorem fpow_two_nonneg
deleted theorem neg_fpow_bit0
deleted theorem neg_fpow_bit1
modified theorem sqr_abs
added theorem pow_bit0_abs
added theorem pow_even_abs
added theorem fzero_pow_eq
added theorem even_bit0
added theorem odd_bit1
added theorem real.fpow_bit0_norm
added theorem real.fpow_even_norm
added theorem real.pow_bit0_norm
added theorem real.pow_even_norm