Commit 2023-03-26 23:21 884393f0

View on Github →

chore: forward-port leanprover-community/mathlib#17895 (#2046) It looks like one of the files in leanprover-community/mathlib#17895 was caught in a race condition and missed the other forward-port.

Estimated changes

added theorem Monotone.pow_right
added theorem StrictMono.pow_right'
added theorem le_max_of_sq_le_mul
added theorem le_of_pow_le_pow'
added theorem lt_max_of_sq_lt_mul
added theorem lt_of_pow_lt_pow'
added theorem min_le_of_mul_le_sq
added theorem min_lt_of_mul_lt_sq
added theorem pow_mono_right
added theorem pow_strictMono_right'
added theorem pow_strictMono_right
deleted theorem strictMono_pow