Commit 2025-01-08 23:18 d4891b46

View on Github →

feat: a ^ n ⊔ b ^ n ≤ (a ⊔ b) ^ n (#20577) From GrowthInGroups (LeanCamCombi)

Estimated changes

added theorem le_pow_sup
added theorem le_self_pow
modified theorem one_lt_pow'
added theorem pow_inf_le
modified theorem pow_le_pow_right'
modified theorem pow_le_pow_right_of_le_one'
modified theorem pow_right_monotone