Commit 2024-09-24 07:14 c15e46e9

View on Github →

chore(Monoid/Unbundled/Pow): cleanup (#17013)

Estimated changes

modified theorem Left.one_le_pow_of_le
modified theorem Left.pow_le_one_of_le
modified theorem Left.pow_lt_one_of_lt
modified theorem Right.pow_le_one_of_le
modified theorem Right.pow_lt_one_of_lt
deleted theorem one_le_pow_of_one_le'
modified theorem one_lt_pow'
deleted theorem pow_le_one'
modified theorem pow_le_pow_left'
deleted theorem pow_lt_one'
modified theorem pow_lt_pow_right'
added theorem pow_right_monotone
modified theorem pow_right_strictMono'