Theorem pow_le_pow_mul_of_sq_le_mul

Modification history

2024-11-26 14:07
Mathlib/Algebra/Order/Monoid/Unbundled/Pow.lean
feat(Pointwise): monotonicity of `pow` (#19252) …
Added pow_le_pow_mul_of_sq_le_mulView on Github →