Commit 2024-10-07 17:59 10671b29

View on Github →

chore: generalise lemmas from OrderedSemiring to MonoidWithZero (#17412) and add the ₀ to follow the naming convention

Estimated changes

deleted theorem mul_le_one₀
added theorem le_self_pow₀
deleted theorem mul_le_one
added theorem mul_le_one₀
added theorem one_le_pow₀
added theorem one_lt_pow₀
added theorem pow_le_one₀
added theorem pow_le_pow_right₀
added theorem pow_lt_one₀
added theorem pow_right_mono₀
added theorem zero_pow_le_one
deleted theorem le_self_pow
deleted theorem one_le_pow₀
deleted theorem one_lt_pow₀
deleted theorem pow_le_one₀
deleted theorem pow_le_pow_right
deleted theorem pow_lt_one₀
deleted theorem pow_right_mono
deleted theorem zero_pow_le_one