Commit 2025-04-10 12:30 7618879b

View on Github →

feat(Order/GroupWithZero): drop more TC assumptions (#23901)

Estimated changes

Modified Mathlib/Algebra/Order/GroupWithZero/Unbundled/Basic.lean

modified theorem Bound.le_self_pow_of_pos

modified theorem Bound.pow_le_pow_right_of_le_one_or_one_le

modified theorem le_self_pow₀

modified theorem mul_le_one₀

modified theorem one_le_pow₀

modified theorem one_lt_pow₀

modified theorem pow_le_of_le_one

modified theorem pow_le_one₀

modified theorem pow_le_pow_iff_left₀

modified theorem pow_le_pow_left₀

modified theorem pow_le_pow_of_le_one

modified theorem pow_le_pow_right₀

modified theorem pow_left_inj₀

modified theorem pow_left_monotoneOn

modified theorem pow_left_strictMonoOn₀

modified theorem pow_lt_one₀

modified theorem pow_lt_pow_iff_left₀

modified theorem pow_lt_pow_left₀

added theorem pow_right_anti₀

modified theorem pow_right_mono₀

modified theorem sq_eq_sq₀

modified theorem sq_le

modified theorem sq_pos_of_pos