Commit 2025-08-14 03:55 639d93da

View on Github →

chore(Algebra/Order): generalize (#28227) Remove some ZeroLEOneClass assumptions. Change some IsStrictOrderedRing to IsOrderedRing. Remove some IsRightCancelAdd and replace some AddLeftStrictMono by AddLeftMono.

Estimated changes

modified theorem pow_le_pow_left₀
modified theorem pow_left_monotoneOn
modified theorem pow_pos
added theorem pow_succ_nonneg
added theorem pow_succ_pos
modified theorem abs_one
modified theorem abs_pow_sub_pow_le
modified theorem abs_two
modified theorem abs_unit_intCast
modified theorem exists_abs_lt
deleted theorem Even.pow_nonneg
modified theorem IsSquare.nonneg
modified theorem not_isSquare_of_neg
modified theorem mul_self_nonneg
modified theorem sq_nonneg
modified theorem sq_nonpos_iff