Commit 2024-11-14 11:04 df8b2f45

View on Github →

chore: generalise pow monotonicity lemmas to groups with zero (#18967) In particular they now apply to ℤₘ₀ From FLT

Estimated changes

deleted theorem pow_lt_pow_right₀
added theorem lt_self_pow₀
added theorem one_le_sq_iff₀
added theorem one_lt_sq_iff₀
added theorem pow_le_pow_iff_left₀
added theorem pow_le_pow_left₀
added theorem pow_left_inj₀
added theorem pow_lt_pow_iff_left₀
added theorem pow_lt_pow_left₀
added theorem pow_lt_pow_right₀
modified theorem pow_pos
added theorem pow_right_injective₀
added theorem pow_right_inj₀
added theorem sq_eq_sq₀
added theorem sq_le_one_iff₀
added theorem sq_lt_one_iff₀
added theorem sq_pos_of_pos
deleted theorem Bound.le_self_pow_of_pos
modified theorem lt_of_mul_self_lt_mul_self
modified theorem lt_self_pow
deleted theorem one_le_pow_iff_of_nonneg
modified theorem one_le_sq_iff
deleted theorem one_lt_pow_iff_of_nonneg
modified theorem one_lt_sq_iff
deleted theorem pow_eq_one_iff_of_nonneg
deleted theorem pow_le_one_iff_of_nonneg
modified theorem pow_le_pow_iff_right
modified theorem pow_le_pow_left
deleted theorem pow_lt_one_iff_of_nonneg
modified theorem pow_lt_pow_iff_right
modified theorem pow_lt_pow_left
modified theorem pow_lt_pow_right
modified theorem pow_lt_self_of_lt_one
modified theorem pow_right_inj
modified theorem pow_right_injective
modified theorem sq_eq_sq
modified theorem sq_le_one_iff
modified theorem sq_lt_one_iff
deleted theorem sq_pos_of_pos