Commit 2022-12-15 21:58 39fe9f89

View on Github →

feat: port Algebra.GroupPower.Order (#1043) from fc2ed6f838ce7c9b7c7171e58d78eaf7b438fb0e have commented out mono annotations as the corresponding tactic is not yet implemented.

Estimated changes

added theorem Left.one_le_pow_of_le
added theorem Left.pow_le_one_of_le
added theorem Left.pow_lt_one_iff'
added theorem Left.pow_lt_one_iff
added theorem Left.pow_lt_one_of_lt
added theorem MonoidHom.map_neg
added theorem MonoidHom.map_neg_one
added theorem MonoidHom.map_sub_swap
added theorem Right.one_le_pow_of_le
added theorem Right.pow_le_one_of_le
added theorem Right.pow_lt_one_iff
added theorem Right.pow_lt_one_of_lt
added theorem abs_le_of_sq_le_sq'
added theorem abs_le_of_sq_le_sq
added theorem abs_lt_of_sq_lt_sq'
added theorem abs_lt_of_sq_lt_sq
added theorem abs_neg_one_pow
added theorem abs_sq
added theorem le_of_pow_le_pow
added theorem le_self_pow
added theorem lt_of_pow_lt_pow
added theorem one_le_pow_iff
added theorem one_le_pow_of_one_le'
added theorem one_le_pow_of_one_le
added theorem one_le_sq_iff
added theorem one_le_zpow
added theorem one_lt_pow'
added theorem one_lt_pow
added theorem one_lt_pow_iff
added theorem one_lt_sq_iff
added theorem pow_abs
added theorem pow_add_pow_le
added theorem pow_bit0_nonneg
added theorem pow_bit0_pos
added theorem pow_bit0_pos_iff
added theorem pow_bit0_pos_of_neg
added theorem pow_bit1_neg
added theorem pow_eq_one_iff
added theorem pow_le_one'
added theorem pow_le_one
added theorem pow_le_one_iff
added theorem pow_le_pow'
added theorem pow_le_pow
added theorem pow_le_pow_iff'
added theorem pow_le_pow_iff
added theorem pow_le_pow_of_le_left'
added theorem pow_le_pow_of_le_left
added theorem pow_le_pow_of_le_one'
added theorem pow_left_inj
added theorem pow_lt_one'
added theorem pow_lt_one
added theorem pow_lt_one_iff
added theorem pow_lt_pow'
added theorem pow_lt_pow
added theorem pow_lt_pow_iff'
added theorem pow_lt_pow_iff
added theorem pow_lt_pow_of_lt_left
added theorem pow_lt_pow_of_lt_one
added theorem pow_lt_pow_succ
added theorem pow_lt_pow₀
added theorem pow_lt_self_of_lt_one
added theorem pow_mono
added theorem pow_pos_iff
added theorem pow_strictMono_left
added theorem sq_abs
added theorem sq_eq_sq
added theorem sq_le_one_iff
added theorem sq_le_sq'
added theorem sq_le_sq
added theorem sq_lt_one_iff
added theorem sq_lt_sq'
added theorem sq_lt_sq
added theorem sq_nonneg
added theorem sq_pos_iff
added theorem sq_pos_of_ne_zero
added theorem sq_pos_of_neg
added theorem sq_pos_of_pos
added theorem strictAnti_pow
added theorem strictMonoOn_pow
added theorem strictMono_pow
added theorem two_mul_le_add_sq
added theorem zero_pow_le_one
deleted theorem sq_nonneg
deleted theorem pow_bit0_nonneg