Commit 2024-11-19 15:36 fa5742c5

View on Github →

feat: a ^ m ≤ b ^ n as a gcongr lemma (#19220) From GrowthInGroups

Estimated changes

Modified Mathlib/Algebra/Order/Monoid/Unbundled/Pow.lean

added theorem pow_le_pow

Modified MathlibTest/GCongr/inequalities.lean